Email Gateway (Aug 18 2022 at 17:36): Email Gateway (Aug 18 2022 at 17:36):From: Stephan Merz <Stephan.Merz@loria.fr>
The TLA+ proof system is based on Isabelle, and Isabelle users are particularly encouraged to apply.
Stephan
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 are developing tools for writing and checking proofs.
TLA+ proofs are interpreted by the Proof Manager (PM), which generates proof obligations corresponding to individual steps of the TLA+ proof. The PM passes proof obligations to backend provers; currently these include the tableau prover Zenon and a generic backend for SMT solvers. When possible, we expect backend provers to produce a detailed proof that is then checked by an axiomatization of TLA+ in the trusted proof assistant Isabelle. In this way, we obtain high assurances of correctness as well as satisfactory automation.
The current version of the PM handles only the "action" part of TLA+: first-order formulas with primed and unprimed variables; where a variable v is considered as unrelated to its primed version v'. This allows us to translate non-temporal proof obligations to standard first-order logic, without the overhead associated with 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 post-doctoral researcher will extend the proof manager to handle the temporal part of TLA+. In cooperation with the other members of the project, he or she will contribute to the extension of the TLA+ proof language to temporal operators, and will design and implement a new translation to Isabelle of the full language. This extension poses interesting conceptual and practical problems. In particular, the new
translation will have to smoothly extend the existing one in order to make use of the plain first-order theorems produced by the old translation, which will be kept for all action-level reasoning.
Skills and profile of the candidate
===================================
The ideal candidate will have a solid knowledge of logic and set theory as well as good implementation skills related to symbolic theorem proving. Of particular relevance are parsing and compilation techniques. Our tools are mainly implemented in OCaml. Experience with temporal and modal logics, Isabelle, Java or Eclipse would be a plus.
Location
========
The Microsoft Research-INRIA Joint Centre is located on the Campus of INRIA Saclay, in the South 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 addresses of one or two references to Damien Doligez <damien.doligez@inria.fr>. The deadline for application is June 1, 2011.
This announcement is available at http://www.msr-inria.inria.fr/Members/doligez/post-doc-position/view
Last updated: Nov 21 2024 at 12:39 UTC