[TYPES/announce] two funded PhD positions at Inria Nancy

[Stephan Merz]

Two PhD positions funded by the ANR projects BLaSST and ICSPA on subjects around formal proofs for set-based specification languages are available at Inria Nancy.


Automated Reasoning for Set Theory (Stephan Merz, Sophie Tourret)
https://urldefense.com/v3/__https://jobs.inria.fr/public/classic/fr/offres/2022-04898__;!!IBzWLUs!UBojhm9so1CW4cg0H9b5fcRYmCe0GK2rsn-6q5HVHbtNwDb4E3ESnFVhwhfIP-cRDyBzABiQ63QP_6ZBiDTR0Gh6mI1Z98jDvVDLww$ 

The main objective is to take advantage of recent progress in automated reasoning for fragments of higher-order logic, and to further contribute to them, specifically for proof obligations generated by the B method.


Formalization of Set Theory and Proof Checking (Stephan Merz, Gilles Dowek)
https://urldefense.com/v3/__https://jobs.inria.fr/public/classic/fr/offres/2022-04909__;!!IBzWLUs!UBojhm9so1CW4cg0H9b5fcRYmCe0GK2rsn-6q5HVHbtNwDb4E3ESnFVhwhfIP-cRDyBzABiQ63QP_6ZBiDTR0Gh6mI1Z98g0wPiTJQ$ 

The thesis will study encoding the set theory of the specification language TLA+ in Dedukti, with the objectives of checking proofs obtained by the TLA+ proof system TLAPS, as well as of enabling interoperability with specifications written in the B language.


More details on the two subjects, as well as information about how to apply, are available at the URLs indicated above. The theses are meant to start in the fall of 2022, the exact starting date is negotiable. I will be very happy to answer any question about the two thesis offers.

Stephan Merz