[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

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.


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 


Candidates should send a resume and the name and e-mail addresses of one or two 
references to Damien Doligez <damien.doli...@inria.fr>. The deadline for 
application is June 1, 2011.

This announcement is available at 

Reply via email to