[Caml-list] Junior engineer position at INRIA Saclay/Ecole Polytechnique, France

[Caml-list] Junior engineer position at INRIA Saclay/Ecole Polytechnique, France

[Kaustuv Chaudhuri]

The Parsifal research team at INRIA Saclay and the Ecole Polytechnique
has an open call for one junior engineer position (2 years).

The main task of the recruited engineer will be to work on the
integration and further development of a number of computational
logic systems designed and built by the team members in recent
years. Some tasks involved are:

 - Designing and implementing a common formal framework for
   communication between the Abella proof assistant, the Bedwyr
   symbolic model checker, and the Tac inductive theorem prover.

 - Using the Teyjus implementation of the Lambda Prolog programming
   language to represent and animate logical specifications of
   deductive and computational systems.

 - Investigating a number of application domains including the formal
   meta-theory of computational systems (programming languages,
   process calculi, etc.), and the use of formal proofs as
   certificates (eg. proof-carrying code, marketplace of proofs).

Candidates should have a bachelor's degree in computer science, be
familiar with the OCaml programming language (or similar high-level
programming languages), and have a background in logic, formal
methods, and symbolic computing.

As this engineer will work with a team of international researchers,
the candidate should be fluent in English. Knowledge of French is
desirable but not mandatory.

The position should begin in October 2011.

Interested candidates are encouraged to contact the following people:

 Dale Miller <dale.miller@inria.fr>.
 Kaustuv Chaudhuri <kaustuv.chaudhuri@inria.fr>

Some links:

Official announcements:
 http://www.lix.polytechnique.fr/parsifal/dokuwiki/doku.php?id=engineer
 http://en.inria.fr/institute/recruitment/offers/young-graduate-engineers

Parsifal team web page:  http://www.lix.polytechnique.fr/parsifal/

System descriptions:
 Bedwyr  http://slimmer.gforge.inria.fr/bedwyr/
 Abella  http://abella.cs.umn.edu/
 Tac     http://slimmer.gforge.inria.fr/tac/
 Teyjus  http://teyjus.cs.umn.edu/