coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] post-doctoral position or 1-year graduate internship -- GUI for TLA+

From: Jean-Jacques Levy <jean-jacques.levy AT inria.fr>
To: caml-list AT inria.fr, types-list AT lists.seas.upenn.edu, mizar-forum AT mizar.uwb.edu.pl, coq-club AT inria.fr, isabelle-users AT cl.cam.ac.uk, hol-info AT lists.sourceforge.net, pvs AT csl.sri.com, twelf-list AT itu.dk
Subject: [Coq-Club] post-doctoral position or 1-year graduate internship -- GUI for TLA+
Date: Sat, 25 Sep 2010 10:34:48 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:from:content-type:content-transfer-encoding:date:subject:to :message-id:mime-version:x-mailer; b=yDtBu2QtdxcNgHj0W85cMgHGZ5+N9FB8ClHCRCH3xk8gpOTFMJGjkGg7YxQpXo7K7d fL2/enSyCgpfCiznPNG/JSIxSeVA5HOLXndYqCnCMT3JQ9LoaNzJdCxjzo+s1J1a6Vhx F3SD0xcS+VmHV4vjJd18LnUnQuujFevbT+gBo=

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:
damien.doligez AT inria.fr,

lamport AT microsoft.com

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

[Coq-Club] post-doctoral position or 1-year graduate internship -- GUI for TLA+, Jean-Jacques Levy