[Caml-list] Coq-related postdoc position at Inria-Saclay

[Caml-list] Coq-related postdoc position at Inria-Saclay

[Bruno Barras]

The Paral-ITP Project (French ANR funding) is looking for candidates
for a 1 year post-doc position, to begin as soon as possible, at
Inria-Saclay, France.

* Position description:

The Paral-ITP Project aims at exploiting the potential of multi-core
processors to improve the user interaction with highly trustable
interactive proof assistants. See the Paral-ITP website for more
information (link below).

The position is focused on the implementation of a distributed kernel
for the Coq proof assistant which would feature the verification of
independent proof-checking tasks concurrently.

* Context :

The successful candidate will work under the supervision of Bruno
Barras and collaborate with Enrico Tassi on the Ecole Polytechnique
campus. He will also have contacts with other teams of the Paral-ITP
Project, namely Fortesse (LRI, Orsay) and Pi.r2 (Inria, Paris).

* Requirements:

Candidates should have a Ph.D. in Computer Science (or give evidence
that the defense is planned soon). They should also be familiar with a
proof assistant in type theory (preferably Coq, Agda or Matita) and be
experienced in the development in a functional programming language
(ML, Haskell). The expertise in concurrency paradigms and the ability
to produce high quality code will be important criteria.

* Application:

Applicants should send an email to Bruno Barras (bruno.barras@inria.fr)
including a CV, a list of publications, and a short (two pages at
most) statement about their research activities. It may also include
the names of up to 2 references.

The deadline for applications is September 15, 2013. Notifications of
acceptance or rejection will be sent out no later than September 30.

* Links:

http://paral-itp.lri.fr/
http://www.inria.fr/centre/saclay