[TYPES/announce] CNRS postdoctoral position in Paris

[Paul-André Melliès]

	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)
-- rewriting theory (rewriting modulo)
-- 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, the institute,
and the new foundation for mathematical sciences in Paris, see

http://www.pps.jussieu.fr
http://www.math.jussieu.fr
http://www.sciencesmaths-paris.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.



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20070410/0045ca8c/attachment.htm