Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
post-doctoral position or 1-year graduate internship -- GUI for TLA+
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2010-09-25 (08:34)
From: Jean-Jacques Levy <jean-jacques.levy@i...>
Subject: post-doctoral position or 1-year graduate internship -- GUI for TLA+

The Microsoft Research-INRIA Joint Centre welcomes applications for a post-doctoral position or graduate internship in the area of tools for interactive theorem proving. The 1-year scholarship can start from fall 2010.

The successful candidate will contribute to the development of the GUI of the TLA+ proof system. TLA+ is Lamport's logic for specification and verification of programs. The system is already developed and distributed at

The candidate should be able to program in Java + Eclipse. Knowledge in mathematical logic is also recommended. The work will be performed inside the "Tools for Formal Specs" group [Damien Doligez, Denis Cousineau, Leslie Lamport, Stephan Merz] at MSR-INRIA Joint Centre in Orsay (south of Paris, France). It will be a prolongation of the interface already developed by Kaustuv Chaudury, Simon Zambrosky, and Dan Ricketts.

Applications should include a curriculum vitae in pdf format and should be sent to

Centre de Recherche Commun INRIA-Microsoft Research,
Parc Orsay Université, 28, rue Jean Rostand, 
91893 Orsay Cedex, France
Telephone: +33 1 69 35 69 70
Fax: +33 1 69 35 69 69

E-mails: damien.doligez*, lamport*

Please email me for any further questions about the position and the related project.