Post doctoral in mechanized theorem proving - 12 months contract

ABOUT TELECOM SUDPARIS

Telecom SudParis is a public graduate school for engineering, which has been recognized on the highest level in the domain of digital technology. The quality of its courses is founded on the scientific excellence of its faculty and on teaching techniques that emphasize project management, innovation and intercultural understanding. Telecom SudParis is part of the Institut Mines-Telecom, the number one group of engineering schools in France, under the supervision of the Minister for Industry. Telecom SudParis with Ecole Polytechnique, ENSTA Paris, ENSAE Paris and Telecom Paris are co-founders of the Institut Polytechnique de Paris, an institute of Science and Technology with an international vocation.

Its assets include: a personalized course, varied opportunities, the no.3 incubator in France, an ICT research center, an international campus shared with Institut Mines-Telecom Business School and over 60 student societies and clubs.

MISSIONS

This position takes place within the 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).

Members of the ICSPA project have developed an encoding of Theory B in Dedukti. In this encoding, it is possible to translate the proof obligations of Atelier B, as well as to search for proofs of these obligations. However, the best solution would be to be able to translate the proofs found by Atelier B directly into Dedukti. To do this, it is proposed that Atelier B should first be instrumented to write a trace containing sufficient information to be able, in a second phase, to reconstruct a complete proof in Dedukti. For this reconstruction, if possible, automated theorem provers able to generate Dedukti proofs will be used.

Furthermore, if there is a Dedukti proof of an encoding of a theory B formula, regardless of how it was obtained, we would like to be able to import it into Atelier B. To do this, we will need to use the mechanisms of Aterlier B to simulate the typing verification performed by Dedukti.

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 ;

• reconstruction of the proof trace in Dedukti ;

• import of Dedukti proofs, using the encoding of B in Dedukti, into Atelier B.

The candidate will collaborate with all people involved in the ICSPA project.

Level of training and / or experience required

• PhD or Doctorat for less than 3 years

Essential skills, knowledge and experience

• Knowledge in logics for computer science

• Experience in mechanized theorem proving

• Good level in programming (if possible, using OCaml)

Advantageous skills, knowledge and experience

• Knowledge of a proof assistants

• Knowledge of the B method

• Knowledge in automated theorem proving

Abilities and skills

• Strong motivation for research

• Ability to work in a team

• Spirit of initiative and creativity, autonomy

APPLICATION PROCEDURE

• Application deadline: February 06th, 2025

• Nature of the contract: 12-months

• Category and profession of the position: II - P, Post-doctoral

• To apply, please send us a CV, a cover letter and a summary of your doctoral thesis

• Location of the position : Evry-Courcouronnes and Palaiseau (France)

• The positions offered for recruitment are open to all with, on request, accommodations for candidates with disabilities

• Working conditions: Teleworking possible, restaurant and cafeteria on site, accessibility by public transport (with employer's participation) or close to main roads, staff association and sports association on campus