post-doctoral position or 1-year graduate internship -- GUI for TLA+
Jean-Jacques Levy <[email protected]>
| Newsgroups | gmane.comp.lang.caml.inria,gmane.comp.mathematics.mizar,gmane.science.mathematics.logic.coq.club,gmane.comp.mathematics.hol |
|---|---|
| Message-ID | <[email protected]> |
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 http://www.msr-inria.inria.fr/Projects/tools-for-formal-specs 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: [email protected], [email protected] Please email me for any further questions about the position and the related project.