[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

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.`