From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 005E1BC57 for ; Sat, 25 Sep 2010 10:34:51 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnkBANZQnUxKfVI0kGdsb2JhbACcAIZCCBUBAQEBCQkTEQMfpjmLUYY1iQMBAQMFhT4EijqCfmCFJ4IO X-IronPort-AV: E=Sophos;i="4.57,234,1283724000"; d="scan'208";a="73429038" Received: from mail-ww0-f52.google.com ([74.125.82.52]) by mail1-smtp-roc.national.inria.fr with ESMTP; 25 Sep 2010 10:34:51 +0200 Received: by wwi17 with SMTP id 17so2092451wwi.9 for ; Sat, 25 Sep 2010 01:34:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:sender:from:content-type :content-transfer-encoding:date:subject:to:message-id:mime-version :x-mailer; bh=FcFCpWa+i7EYogQ1JP29oKWx2r42AQtkLNM17nig0vk=; b=H3sbT3lnkndjJ4eiqfg/Jk7YVDJRqqQrpG/cIo76CRDEC1VaBjDi0y9K+00ufHvDPE hMjxP/E8HT+yiRQaUeL3GvGISjL9AR9/JPVXrT8vepX+3Rc0ltaV4emTMJLOYjGXMynM Q4jHSFo9rfnOQD2estCdhf6bNWpUCMQV1kKL0= 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= Received: by 10.216.51.66 with SMTP id a44mr893897wec.7.1285403691276; Sat, 25 Sep 2010 01:34:51 -0700 (PDT) Received: from [192.168.0.27] (85-169-73-131.rev.numericable.fr [85.169.73.131]) by mx.google.com with ESMTPS id p45sm1928319weq.45.2010.09.25.01.34.49 (version=TLSv1/SSLv3 cipher=RC4-MD5); Sat, 25 Sep 2010 01:34:50 -0700 (PDT) Sender: =?UTF-8?B?SmVhbi1KYWNxdWVzIEzDqXZ5?= From: Jean-Jacques Levy Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Date: Sat, 25 Sep 2010 10:34:48 +0200 Subject: post-doctoral position or 1-year graduate internship -- GUI for TLA+ To: caml-list@inria.fr, types-list@lists.seas.upenn.edu, mizar-forum@mizar.uwb.edu.pl, coq-club@inria.fr, isabelle-users@cl.cam.ac.uk, hol-info@lists.sourceforge.net, pvs@csl.sri.com, twelf-list@itu.dk Message-Id: Mime-Version: 1.0 (Apple Message framework v1081) X-Mailer: Apple Mail (2.1081) X-Spam: no; 0.00; damien:01 orsay:01 prolongation:01 orsay:01 rostand:01 damien:01 leslie:98 28,:98 doligez:01 doligez:01 cousineau:01 theorem:02 universite:02 cedex:02 gui:03 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=20 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=E9, 28, rue Jean Rostand,=20 91893 Orsay Cedex, France Telephone: +33 1 69 35 69 70 Fax: +33 1 69 35 69 69 E-mails: damien.doligez@inria.fr, lamport@microsoft.com Please email me for any further questions about the position and the = related project.