Context
One or two postdoctoral positions are available within the Parsifal team, a joint research team between INRIA Saclay and the Laboratoire d’Informatique (LIX) on the campus of Ecole Polytechnique.
Successful candidates will help with designing, implementing, and experimentally validating the design of proof certificates for a range of theorem provers in intuitionistic and classical logic and arithmetic. These positions are for one year, with a second year extension possible. Candidates should start in Fall 2013.
These positions are funded by ProofCert, an ERC Advanced Grant with the goal of designing 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 as well as supporting (bounded) proof reconstruction.
The ideal candidate should have strong backgrounds in
- basic proof theory (in particular, the sequent calculus);
- various automated and interactive theorem proving systems (particularly those involving induction); and
- programming in logic programming (Prolog or lambda Prolog) as well as other high-level programming languages (such as ML or Haskell).
Venue
Employed postdocs will be members of the INRIA Parsifal team which is located in the Laboratoire d’Informatique (LIX) on the campus of Ecole Polytechnique. This campus is situated to the south of Paris and is an easy commute from Paris on the RER B regional train line. French proficiency is not a requirement.
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@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 in mid-April 2013.
More Information
Further information regarding ProofCert and the Parsifal team can be found at the following urls.
- The ERC Advanced Grant ProofCert
- The INRIA Parsifal team
- Positions offered by Parsifal in 2013
- Miller’s web page
