Email Gateway (Aug 18 2022 at 11:55): Email Gateway (Aug 18 2022 at 11:55):From: Xavier Urbain <urbain@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
Last updated: May 03 2024 at 04:19 UTC