PostDoc available at LIX, Ecole Polytechnique, France

The following postdoc position is available at the LIX labs on the campus
of Ecole Polytechnique, France.

*PostDoc: Designing and implementing proof certificates*

*Context*

ProofCert is a recently awarded ERC Advanced Grant that will be funded for
the five years 2012-2016. The goal of ProofCert is to design a format for
proof certificates that can capture the proof evidence within all major
theorem provers while also being checkable by a simple, declarative proof
checker. This format must allow treating some inference steps as
(non-deterministic) computation and as well as supporting (bounded) proof
reconstruction.

A postdoctoral position is available within the ProofCert project. This
position is concerned with helping to design, implement, and experimentally
validate the design of proof certificates for a range of theorem provers in
classical first-order logic. The position is for one year, with a second
year extension possible.  It should start in Fall 2012.

The ideal candidate should have strong backgrounds in

   - basic proof theory (in particular, the sequent calculus);
   - various automated and interactive theorem proving systems; and
   - programming in logic programming (Prolog or lambda Prolog) as well as
   other high-level programming languages (such as ML or Haskell).


*Venue*

The postdoc will be a member of the INRIA Parsifal team and will work in a
new building on the campus of the Ecole Polytechnique that houses the
Laboratoire d’Informatique (LIX). This campus is situated to the south of
Paris, an easy commute from Paris on the RER B regional train line. French
proficiency is not necessary.

*Application*

Candidates must have a Ph.D.; if the Ph.D. thesis is not yet defended when
the application is made, the candidate should provide the planned defense
date and the composition of the thesis committee.

To apply, contact Dale Miller (dale.miller at inria.fr) and include a cover
letter and (links to) your CV and publication list. Additional material,
such as letters of recommendation, will be requested if necessary. Early
expression of interest is encouraged.  We plan to make a decision on this
position around the beginning of April 2012.

*More Information*

Further information regarding ProofCert and the Parsifal team can be found
at the following links.
- The ERC Advanced Grant ProofCert: http://team.inria.fr/parsifal/proofcert/
- The INRIA Parsifal team: http://team.inria.fr/parsifal/
- Positions offered by Parsifal in 2012:
http://team.inria.fr/parsifal/positions/
- Miller's web page: http://www.lix.polytechnique.fr/Labo/Dale.Miller/

_______________________________________________
Lprolog mailing list
[email protected]
https://wwws.cs.umn.edu/mm-cs/listinfo/lprolog