[No longer available.]
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@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 INRIA Parsifal team
– The ERC Advanced Grant ProofCert
– Technical description of ProofCert (this postdoc corresponds roughly to tasks T2 and T3)
