[TYPES/announce] Junior engineer position at INRIA Saclay/Ecole Polytechnique, Paris, France
kaustuv.chaudhuri at inria.fr
Mon Jun 20 15:35:16 EDT 2011
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 at inria.fr>.
Kaustuv Chaudhuri <kaustuv.chaudhuri at inria.fr>
Parsifal team web page: http://www.lix.polytechnique.fr/parsifal/
More information about the Types-announce