Email Gateway (Aug 18 2022 at 11:03): Email Gateway (Aug 18 2022 at 11:03):From: Xavier Urbain <urbain@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@lri.fr>
Xavier Urbain <urbain@ensiie.fr>
A3PAT webpage:
http://www.ensiie.fr/~urbain/a3pat/
PROVAL webpage:
http://proval.lri.fr
Last updated: May 03 2024 at 08:18 UTC