[Axiom-developer] PostDoc Position

[Tim Daly]

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 over ten years, the proof language is more recent,
and we are developing 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 SMT solvers, 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. Because Isabelle 
considers a variable to be unrelated to its primed version, the PM can 
translate first-order formulas to first-order formulas, 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 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 or she will have to define and 
implement a new translation into Isabelle to handle the temporal operators in a 
way that enables the use of TLA+ proof rules whose hypotheses include both 
temporal-logic formulas and non-temporal theorems proved with the simple 
translation.

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.

Ideally, the candidate will start working in september or october, but we can 
accomodate a later date.

Contact

Candidates should send a resume and the name and e-mail address of one or two 
references to Damien Doligez <address@hidden>.