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.