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 Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 7BDEDBC68 for ; Mon, 6 Nov 2006 09:38:44 +0100 (CET) Received: from [128.93.11.95] (estephe.inria.fr [128.93.11.95]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id kA68cipn028274 for ; Mon, 6 Nov 2006 09:38:44 +0100 Message-ID: <454EF494.3050305@inria.fr> Date: Mon, 06 Nov 2006 09:38:44 +0100 From: Xavier Leroy User-Agent: Mozilla Thunderbird 1.0.6-6mdk (X11/20050322) X-Accept-Language: en-us, en MIME-Version: 1.0 To: caml-list@inria.fr Subject: Post-docs on formal compiler verification X-Enigmail-Version: 0.92.0.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 454EF494.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; compiler:01 high-level:01 subset:01 semantics:01 coq:01 semantics:01 compiler:01 coq:01 subset:01 damien:01 letouzey:01 evry:01 antipolis:01 analyzers:98 1800:98 [ The following openings might interest members of this list, as it is strongly concerned with (mechanized proofs of) pure functional programs. - Xavier Leroy ] The Compcert project, funded by the French National Agency for Research in its program on the security of computer systems (ANR-SSIA), is offering two post-doctoral positions for durations of up to 18 months, starting in the first half of 2007. The Compcert project is concerned with the formal description of optimizing compilers for high-level languages, including a significant subset of the C programming language, and computer-verified proofs of correctness for these compilers. Foundational aspects of this project include the mechanization of programming language semantics and mechanically verified proofs of correctness for functional and imperative programs. Most proofs and algorithms are verified using the Coq proof assistant. The project is looking for applicants having a solid background in one or preferably two of the following domains: * programming language semantics, * compiler development, * computer-based proof assistants, and a real interest in the other aspects. The topics to be investigated during the post-docs range over the scope of the project, from formal compiler verification to mechanized semantics to connections with other tools (program provers, static analyzers) used to develop high-assurance software. For instance, we envision the following two topics: * A formalization of domain theory inside the type theory of the Coq proof assistant and a study of its applications in the development of correct functional programs, with a special focus on potentially non-terminating programs such as interpreters, debuggers, or semi-algorithms for optimisation problems. * A study of separation logic for the Compcert subset of the C programming language, including formal proofs of consistency between this axiomatic semantics and the operational semantics used in the compiler verification task. Proposals for other relevant topics are welcome and will be discussed between applicants and the investigators of the Compcert project: Xavier Leroy (INRIA, main investigator), Yves Bertot (INRIA), Sandrine Blazy (ENSIIE), Pierre Courtieu (CNAM), Damien Doligez (INRIA), Pierre Letouzey (University of Paris 7), Laurence Rideau (INRIA). The positions are located either in Evry (Paris area, under the supervision of Sandrine Blazy) or Sophia Antipolis (Nice area, French Riviera, under the supervision of Yves Bertot). The gross salary is around 2200 Euros per month (1800 Euros net salary after deduction of social benefits). To apply, please send a detailed vitae and a research statement (indicating the topics on which you'd like to work) to the following address: compcert@yquem.inria.fr. Other inquiries concerning these positions can be sent to this address as well.