The Coq mailing list

[Stephan Merz <Stephan.Merz AT loria.fr>]

I originally posted this announcement a while ago, but due to some requests 
we received, we decided to extend the application deadline to May 15. If you 
are interested, please send us your application. Informal inquiries are also 
welcome.

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 contribute to a proof development environment for 
TLA+ developed in the Tools for Proofs project (see 
http://www.msr-inria.inria.fr).

Research Context
================

TLA+ is a language for specifying and reasoning about systems, including 
concurrent and distributed systems.  It is based on first-order logic, set 
theory, temporal logic, and a module system. TLA+ and its tools have been 
used in industry for over a decade.  More recently, we have extended TLA+ to 
include hierarchically structured formal proofs that are independent of any 
proof checker.  We have released several versions of the TLAPS proof checker 
(http://msr-inria.inria.fr/~doligez/tlaps/) and integrated it into the TLA+ 
Toolbox, an IDE for the TLA+ tools 
(http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html).

TLAPS and the Toolbox support the top-down development of proofs and the 
checking of individual proof steps independently of the rest of the proof.  
This helps users focus on the part of the proof they are working on.  
Although still lacking important features, TLAPS is already a powerful tool 
and has been used for a few verification projects, including a proof of the 
safety properties of a Byzantine-fault tolerant consensus algorithm 
(http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html).

TLAPS consists of the Proof Manager (PM, an interpreter for the proof 
language that computes the proof obligations corresponding to each proof 
step) and an extensible list of backend provers. Current backends include the 
tableau prover Zenon, an encoding of TLA+ as an object logic in the Isabelle 
proof assistant, and a generic backend for SMT solvers. When possible, we 
expect backend provers to produce a detailed proof that is then checked by 
Isabelle.  In this way, we can obtain high assurance 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 to be 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.

Description of the activity of the post-doc
===========================================

You will work with other members of the project, including Leslie Lamport, 
Damien Doligez, and Stephan Merz, on the extension of the TLA+ proof language 
to temporal operators.  This extension poses interesting conceptual and 
practical problems.  In particular, the new translation must smoothly extend 
the existing one since temporal proof steps rely on action-level subproofs.  
You will have the primary responsibility for designing and implementing 
algorithms to generate corresponding proof obligations.

As time permits and depending on your interests, you will have the 
opportunity to contribute to further improving the proof checker. 
This may include:
- adding support for certain TLA+ features that are not yet handled by the 
PM, such as recursive operator definitions and elaborate patterns  for 
variable bindings;
- finding what improvements are needed by verifying real examples, perhaps 
including liveness of the aforementioned consensus algorithm;
- integrating new backends to improve the automation of proofs;
- adding validation of proofs by backends whose proofs are not now checked.

Skills and profile of the candidate
===================================

You should 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.

Given the geographical distribution of the members of the team, we highly 
value a good balance between the ability to work in a team and the capacity 
to propose initiatives.

Location
========

The Microsoft Research-INRIA Joint Centre is located on the Campus of INRIA 
Saclay south of Paris, near the Le Guichet RER station.

Starting date
=============

The normal starting date of the contract would be September 2012, but we can 
arrange for an extremely well-qualified candidate to start sooner.

Contact
=======

Candidates should send a resume and the name and e-mail addresses of one or 
two references to Damien Doligez 
<damien.doligez AT inria.fr>.
 The deadline for application is May 15, 2012.

This announcement is available at
< http://www.msr-inria.inria.fr/Members/doligez/post-doc-position-2012/view ;>