Postdoctoral Research Associate: Telecom SudParis invites applications for a Postdoctoral Research Associate position in mechanized theorem proving. The role is part of the ANR project ICSPA, focusing on improving trust in proof assistants based on set theory. The candidate will work on the Atelier B tool developed by Clearsy and collaborate on the export and import of proofs between different proof assistants using the Dedukti logical framework.
Postdoctoral Research Associate in Mechanized Theorem Proving – 12 Months Contract
Designation: Postdoctoral Research Associate
Research Area: Mechanized Theorem Proving
Location: Evry-Courcouronnes, Île-de-France, France
Eligibility/Qualification:
- PhD or Doctorat for less than 3 years
- Knowledge in logics for computer science
- Experience in mechanized theorem proving
- Good level in programming, preferably using OCaml
- Knowledge of proof assistants, the B method, and automated theorem proving is advantageous
- Strong motivation for research
- Ability to work in a team
- Initiative, creativity, and autonomy
Job Description: The candidate will:
- Work with Clearsy to instrument the Atelier B tool to recover a proof trace
- Reconstruct the proof trace in Dedukti
- Import Dedukti proofs into Atelier B using the encoding of B in Dedukti
- Collaborate with the ICSPA project team
How to Apply:
- Application Deadline: March 5th, 2024
- Contract: 12-months
- Category and Profession: II – P, Post-doctoral
- Send CV, cover letter, and a summary of your doctoral thesis to guillaume.burel@ensiie.fr
- Location: Evry-Courcouronnes and Palaiseau, France
Last Date for Apply: 05 March 2024
Disclaimer: This job post is based on information obtained from a reliable source. Applicants are encouraged to check the official Telecom SudParis website for further details and to verify the accuracy of the information provided.
