The Coq mailing list

[Xavier Urbain <urbain AT ensiie.fr>]

Trustworthy decision procedures

A 12 months post-doc  position, starting *December 2007*, is available
inside  the  A3PAT   project,  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://www.ensiie.fr/~urbain/a3pat/

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




-- 

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

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