[isabelle] Post-doc position (Paris and Orsay) Trustworthy Decision Procedures

  Trustworthy decision procedures

A 12 months post-doc position, starting June 2008, is available inside
the A3PAT project (http://a3pat.ensiie.fr), regarding Certification of
Automated Proofs. The post is  based in the PROVAL project (Orsay) and
in the CÉDRIC lab. (CNAM Paris).

  We aim  at helping proof-assistants with  trustworthy automation, in
particular  by means of  proof traces  from which  proof terms  may be

  The post-doc researcher  is asked to focus on  some of the following
topics regarding AC unification:

   * Elementary case (involving Diophantine equations)

   * Combination  (restricted to  the simpler case of disjoint symbols 
     and collapse free)

   * Applications to properties of Term Rewriting Systems
     (eg. termination: AC compatible orderings, etc.)

Results will be  implemented so as to ensure  proof delegation between
proof-assistants and automated provers.

Skills   in  an   ML-like  language   and  First   Order   Logics  are
mandatory.  Experience in  term rewriting  and  proof-assistants (Coq,
Isabelle/HOL,  PVS,  etc.)  would  be  a  clear  plus.   

Contacts and information:

    * Évelyne Contejean   contejea[_at_]lri.fr
    * Xavier Urbain   urbain[_at_]ensiie.fr 

A3PAT webpage:

PROVAL webpage:


Xavier Urbain

C.N.A.M. -- E.N.S.I.I.E.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.