[ 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: compc...@yquem.inria.fr.  Other inquiries concerning these
positions can be sent to this address as well.

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs