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.1 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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 06DB5BC37 for ; Tue, 9 Jun 2009 13:50:43 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.41,331,1241388000"; d="scan'208";a="30841849" Received: from 250-95.msr-inria.inria.fr (HELO [10.0.1.199]) ([193.55.250.95]) by mail1-relais-roc.national.inria.fr with ESMTP/TLS/AES128-SHA; 09 Jun 2009 13:50:42 +0200 Message-Id: <1DEC3054-1D3A-4449-8868-BDD6C3292FEC@inria.fr> From: Damien Doligez To: caml users Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v935.3) Subject: JOB: post-doc at MSR-INRIA Joint Centre Date: Tue, 9 Jun 2009 13:50:42 +0200 X-Mailer: Apple Mail (2.935.3) X-Spam: no; 0.00; damien:01 damien:01 post-doc:01 first-order:01 low-level:01 trivial:01 first-order:01 post-doc:01 re-use:01 theorems:01 compilation:01 ocaml:01 leslie:98 leslie:98 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. The main program of our development environment is called the Proof Manager (PM). The PM translates TLA+ source files to low-level proofs that are checked by Isabelle. To this end, the PM calls the Zenon automatic theorem prover to fill in the "trivial" details omitted from proofs at the source level. Within the Isabelle framework we have an axiomatization of TLA+ (Isabelle/TLA+). Isabelle provides high assurance by checking all the proofs provided by the user or by Zenon. The PM also has an interface to CVC3, which provides a stronger automatic prover, but with lower assurance of correctness. The current version of the PM handles only the "action" part of TLA+: first-order formulas with primed and unprimed variables; where a variable is considered as unrelated to its primed version. This allows us to translate first-order formulas to first-order formulas, without the overhead associated to an encoding of temporal logic into first-order logic. This part of TLA+ is already useful for proving safety properties. Description of the activity of the post-doc The task devoted to the post-doc will be to extend the proof manager to deal with the temporal part of TLA+. To this end, he will have to define a new translation into Isabelle to handle the temporal operators, in a way that enables the re-use of non-temporal theorems proved with the simple translation. He will also have to implement this new translation and the interface between the two translations. 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 and the name and e-mail address of one or two references to Damien Doligez .