Email Gateway (Feb 16 2024 at 21:30): Email Gateway (Feb 16 2024 at 21:30):From: Guillaume Burel <guillaume.burel@ensiie.fr>
Dear all,
The link to apply to the position and to get more information was
erroneous. Please go to:
https://institutminestelecom.recruitee.com/l/en/o/postdocenpreuvemecanisee
Sorry for the inconvenience.
Guillaume Burel
Le 16/02/2024 à 11:19, Guillaume Burel a écrit :
The following post-doctoral position has been reopened until March 5th. The starting date can be up to July. Please apply online at
https://institutminestelecom.recruitee.com/l/en/o/postdocenpreuvemecanisee
Do not hesitate to transfer this offer to anyone interested.
Post-doctoral position in mechanized theorem proving - 12 months
Laboratory Samovar, Institut Polytechnique de Paris,
Telecom SudParis, Évry-Courcouronnes, FranceThe position can take place at Évry and/or on the Paris-Saclay campus.
Detailed information and candidacy here:
https://institutminestelecom.recruitee.com/l/en/o/postdocenpreuvemecanisee
Context
=======This position takes place within the French ANR project ICSPA (http://icspa.inria.fr/), which seeks to improve trust in proof assistants based on set theory (B method, TLA+). To do this, the idea is to export proofs found by such tools into the Dedukti logical framework, and also to import proofs from Dedukti into these assistants. By having the proof verified in Dedukti, we increase confidence in what the assistant claims. In the other direction, this enables the proofs to be certified for industrial use. Finally, by moving down from one assistant to Dedukti and then up again to another, this enables interoperability between them.
This position focuses on the Atelier B tool developed by Clearsy (a member of the ANR project consortium).
Activities
==========The candidate will be required to carry out the following tasks:
- working with Clearsy to instrument the Atelier B tool in order to recover a proof trace ;
- from such trace, reconstruction of a proof in Dedukti ;
- reciprocally, import of Dedukti proofs into Atelier B.
The candidate shall collaborate with all people involved in the ICSPA project.
Job requirements
================Experience in logic in computer science, mechanized theorem proving, and good level in programming (if possible, using OCaml) are requested.
In addition, knowledge of a proof assistants, of the B method and/or in automated theorem proving will be appreciated.
Application
===========Candidates should apply online at
https://institutminestelecom.recruitee.com/l/en/o/postdocenpreuvemecanisee
before March 5th, 2024.
To apply, please send us a CV, a cover letter and a summary of your doctoral thesis.
For more information, please contact Guillaume Burel <guillaume.burel@ensiie.fr>.
Last updated: Jan 04 2025 at 20:18 UTC