The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

The Marelle team at INRIA Sophia Antipolis concentrates on various
aspects of computer-aided proof verification.  It participates to two
major efforts for formalizing mathematics: the Math-Components effort,
which aims at understanding how to structure large libraries of
formal development, with a landmark objective focused on the
Feit-Thompson theorem (a theorem in Group theory) and the Formath
project, which is an Europe-wide effort on the formalization of
mathematics, with a strong focus on linear algebra and its application
to algebraic topology and numeric computation.  The Marelle team also
investigates applications of formalized mathematics in the
verification of cryptographic primitives and extensions of Type-Theory
based systems with extra computation powers and connections to SMT
solvers.

The team invites applications for post-doc positions of approximately
one year on topics related to its focus.  Applicants should exhibit a
balanced knowledge of mathematics and computer-science and should be
aware that most of the tasks envision during the post-doctoral period
will revolve around proof development using the Coq system.

Applications should be sent to Yves Bertot and Nathalie Bellesso,

Yves.Bertot AT inria.fr
Nathalie.Bellesso AT inria.fr

Applications should include

- a complete C.V.

- references to at most three publications considered by the author as
their most significant scientific production.  If the most significant
production is in the form of running software, this software and
documentation should be made available.

- Names of well-known researchers that would be willing to write
  recommendation letters in support of the applicant (at most 5).