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: damien....@inria.fr, lam...@microsoft.com
Please email me for any further questions about the position and the related project.
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs