Email Gateway (Aug 18 2022 at 13:35): Email Gateway (Aug 18 2022 at 13:35):From: Damien Doligez <damien.doligez@inria.fr>
Research team: Tools for Proofs, MSR-INRIA Joint Centre
The Microsoft Research-INRIA Joint Centre is offering a 2-year
position for a post-doctoral researcher to work on a proof development
environment for TLA+ in the Tools for Proofs project-team (see
http://www.msr-inria.inria.fr).
Research Context
TLA+ is a language for formal specifications and proofs designed by
Leslie Lamport. It is based on first-order logic, set theory,
temporal logic, and a module system. While the specification part of
TLA+ has existed for several years, the proof language is more recent,
and we want to develop tools for writing and checking proofs.
The main program of our development environment is called the Proof
Manager (PM). The PM translates TLA+ source files to low-level proofs
that are checked by Isabelle. To this end, the PM calls the Zenon
automatic theorem prover to fill in the "trivial" details omitted from
proofs at the source level. Within the Isabelle framework we have an
axiomatization of TLA+ (Isabelle/TLA+). Isabelle provides high
assurance by checking all the proofs provided by the user or by Zenon.
The PM also has an interface to CVC3, which provides a stronger
automatic prover, but with lower assurance of correctness.
The current version of the PM handles only the "action" part of TLA+:
first-order formulas with primed and unprimed variables; where a
variable is considered as unrelated to its primed version. This
allows us to translate first-order formulas to first-order formulas,
without the overhead associated to an encoding of temporal logic into
first-order logic. This part of TLA+ is already useful for proving
safety properties.
Description of the activity of the post-doc
The task devoted to the post-doc will be to extend the proof manager
to deal with the temporal part of TLA+. To this end, he will
have to define a new translation into Isabelle to handle the temporal
operators, in a way that enables the re-use of non-temporal theorems
proved with the simple translation. He will also have to implement
this new translation and the interface between the two translations.
Skills and profile of the candidate
We are looking for a candidate with skills in some or all of the
following subjects: parsing and compilation, logic and set theory,
Isabelle, OCaml, Eclipse and Java. Moreover, the applicant must have
a good command of the English language.
Location
The Microsoft Research-INRIA Joint Centre is located on the Campus of
INRIA Futurs, in South part of Paris, near the Le-Guichet RER
station. The Tools for Proofs project-team is composed of Damien
Doligez, Leslie Lamport and Stephan Merz.
Contact
Candidates should send a resume and the name and e-mail address
of one or two references to Damien Doligez <damien.doligez@inria.fr>.
Last updated: May 03 2024 at 08:18 UTC