From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id AB2D0BC69 for ; Wed, 21 Feb 2007 15:24:43 +0100 (CET) Received: from [128.93.8.130] (macadam.inria.fr [128.93.8.130]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l1LEO8oS029481 for ; Wed, 21 Feb 2007 15:24:43 +0100 Mime-Version: 1.0 (Apple Message framework v752.2) Content-Transfer-Encoding: 7bit Message-Id: <1564711F-6674-4C51-B0AD-A3C78811C855@inria.fr> Content-Type: text/plain; charset=US-ASCII; format=flowed To: caml users From: Damien Doligez Subject: opening for a post-doc at the MSR-INRIA joint centre Date: Wed, 21 Feb 2007 15:24:45 +0100 X-Mailer: Apple Mail (2.752.2) X-Miltered: at concorde with ID 45DC5608.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; damien:01 damien:01 post-doc:01 first-order:01 translated:01 low-level:01 trivial:01 post-doc:01 parsing:01 compilation:01 ocaml:01 leslie:98 leslie:98 doligez:01 doligez:01 Research team: Tools for Proofs, MSR-INRIA Joint Centre The Microsoft Research-INRIA Joint Centre is offering a 2-year position for a post-doctoral researcher to work on a proof development environment for TLA+ in the Tools for Proofs project-team (see http://www.msr-inria.inria.fr ). Research Context TLA+ is a language for formal specifications and proofs designed by Leslie Lamport. It is based on first-order logic, set theory, temporal logic, and a module system. While the specification part of TLA+ has existed for several years, the proof language is more recent, and we want to develop tools for writing and checking proofs. Our development environment for TLA+ proofs will have the following structure: TLA+ source files will be translated to low-level proofs that will be checked by Isabelle. These will include calls to the Zenon automatic theorem prover to fill in the "trivial" details omitted from proofs at the TLA+ level. Within the Isabelle framework we will have an axiomatization of TLA+ (Isabelle/TLA+). Isabelle will provide high assurance by checking all the proofs provided by the user or by Zenon. As the user writes and modifies the TLA+ source code, a proof manager will keep track of which parts of the proofs need to be modified and re-checked by Isabelle. The proof manager will also support direct interaction from the user with Isabelle when needed. Description of the activity of the post-doc The task devoted to the post-doc will be to develop the tools that make up the TLA+ development environment: the translator to Isabelle, the Zenon-Isabelle interface, and the proof manager. He will also complete the development of the TLA+ theory in the Isabelle framework (Isabelle/TLA+), which is currently incomplete. Skills and profile of the candidate We are looking for a candidate with skills in some or all of the following subjects: parsing and compilation, logic and set theory, Isabelle, OCaml, Eclipse and Java. Moreover, the applicant must have a good command of the English language. Location The Microsoft Research-INRIA Joint Centre is located on the Campus of INRIA Futurs, in South part of Paris, near the Le-Guichet RER station. The Tools for Proofs project-team is composed of Damien Doligez, Leslie Lamport and Stephan Merz. Contact Candidates should send a resume to Damien Doligez .