The Coq mailing list

[Jean-Jacques Levy <jean-jacques.levy AT inria.fr>]

Friends, please consider the following announcement. -JJ-

-------------------------------------------------------------------

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 <damien.doligez AT inria.fr>.