[TYPES/announce] Postdocs available in Proof Certificates

[Dale Miller]

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 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 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: http://team.inria.fr/parsifal/proofcert/
- The INRIA Parsifal team: http://team.inria.fr/parsifal/
- Positions offered by Parsifal in 2013:
http://team.inria.fr/parsifal/positions/
- Miller's web page: http://www.lix.polytechnique.fr/Labo/Dale.Miller/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20130314/ec8d012b/attachment.html>