[Caml-list] [JOB] post-doc position available at MSR-INRIA in France

[Caml-list] [JOB] post-doc position available at MSR-INRIA in France

[Damien Doligez]

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 announce is available at
< http://www.msr-inria.inria.fr/Members/doligez/post-doc-position/view >