19 Sep 2023Job Information
TSP - Telecom SudParis
Electronics and Physics dept. (EPh)
First Stage Researcher (R1)
18 Oct 2023 - 00:00 (Europe/Paris)
Type of Contract
Hours Per Week
Offer Starting Date
19 Oct 2023
Is the job funded through the EU Research Framework Programme?
Not funded by an EU programme
Is the Job related to staff position within a Research Infrastructure?
This position takes place within the ANR project ICSPA (https:// 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.
The candidate will be required to carry out the following tasks:
The candidate will collaborate with all people involved in the ICSPA project.Requirements
PhD or equivalent
Skills/QualificationsLevel of training and / or experience required
Essential skills, knowledge and experience
Website for additional job details
https: // institutminestelecom.recruitee.com/l/en/o/offre-type-telecom- sudparis-t…Work Location(s)
Number of offers available
9 rue Charles FOURIER
GeofieldWhere to apply
https: // institutminestelecom.recruitee.com/l/en/o/offre-type-telecom- sudparis-t…Contact
https: // www. telecom-sudparis.eu/
9 rue Charles FOURIER
Post Doctoral In Mechanized Theorem Proving - 12 Months Contract
Universities and Institutes of France
September 20, 2023
October 18, 2023
Computer Science,Engineering,Physics,Space Science