[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
