The Coq mailing list

[Xavier Urbain <urbain AT ensiie.fr>]

  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
generated.

  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:
http://a3pat.ensiie.fr

PROVAL webpage:
http://proval.lri.fr

-- 

Xavier Urbain
-----------------------------------------------------------------
CEDRIC, CPR

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