CNRS postdoctoral position in Paris

[Paul-Andre Mellies <paul-andre.mellies@pps.jussieu.fr>]

	CNRS POSTDOCTORAL POSITION ANNOUNCEMENT

A one-year postdoctoral fellowship in mathematics and computer science
has been opened by the CNRS for the next academic year.

The purpose of the postdoc position is to work in our research team PPS
(Proofs, Programs, Systems) on a project at the interface between

-- proof theory (linear logic)
-- type theory (dependent types)
-- homotopy theory (model structures)
-- category theory (higher dimensional categories)

The more detailed research project appears below.

The postdoc position will take place at the Institut Mathematique de
Jussieu,
a very large and lively mathematical research institute situated in
Paris centre.

The deadline for submission is 10 MAY 2007.

Potential applicants should contact us as early as possible

Pierre-Louis Curien (curien at pps.jussieu.fr)
Paul-Andre Mellies (mellies at pps.jussieu.fr)

For more information about the PPS research group and the institute, see
http://www.pps.jussieu.fr
http://www.math.jussieu.fr

------------------------------------------------------------------------
--------------------------------------------

Research project

Type theory plays a fundamental role in the definition of programming
languages
and proof systems. More specifically, dependent type theory
introduced by Martin-Lof
in the 1970s lies at the heart of many proof assistants, like the Coq
system developed
at INRIA.

Recently, a promising meeting point has emerged between dependent
type theory,
and homotopy theory -- a theory embracing all of algebraic topology.
The basic idea
is simple: the typing towers encountered in type theory, where a
program M has a type tau,
which itself has a class s... are of the same nature as the homotopy
towers, where
two paths f and g of dimension 1 are related by homotopy relations
alpha and beta
of dimension 2, themselves related by homotopy relations of dimension
3, etc.
However, this meeting point between type theory and homotopy theory
can only be reached
at the price of abstraction, using the higher dimensional category
theory.

We are convinced that this homotopic point of view leads eventually
to a better integration
of type theory (dependent types), proof theory (linear logic), and
rewriting theory (rewriting modulo).

Profile of the candidate

The candidate will have an expertise in at least one of the following
fields: proof theory,
type theory, rewriting theory, homotopy theory, higher dimensional
category theory.
He will also be curious to learn the other fields, and to work at
their interface.