Post-doctoral position at LIPN, Université Paris 13,
Implicit computational complexity and linear logic
A 12-month post-doctoral position is vacant at the Laboratoire d’Informatique de Paris Nord (LIPN), Université Paris 13, within the research project COMPLICE (Implicit Computational Complexity, Concurrency and Extraction), funded by the French national research agency (ANR).
Please note that the position is to be filled relatively quickly, so the deadline is quite short :
deadline for applications : 12 July 2011 (next week !) notification : 13 July 2011 starting date : 1 October 2011 (no later than 1 Dec 2011)
COMPLICE is a four-year project whose partner sites are ENS Lyon, Université Paris 13 and LORIA-Nancy. The project’s goal is to investigate the foundations and applications of implicit computational complexity (ICC), along the lines of semantics and logic, functional programming, program extraction from proofs, quantitative properties and ICC for concurrent systems.
LIPN plays a major role in research in computer science within the northern Paris area. The post-doc researcher will work within the Logic, Computation and Reasoning group, among whose main research directions there are proof theory, linear logic, lambda-calculus, implicit computational complexity, denotational semantics, and system specification and verification. LIPN is situated in Villetaneuse, in the northern suburbs of Paris, within the campus of the University Paris 13 (about 45 minutes from the city center by public transportation).
Interaction with the other sites of the COMPLICE project is possible, as with other sites in the Paris area (PPS, LIX, etc.).
Salary and benefits
The monthly salary will be around 2000 EUR. This is then subject to income tax. The position is for 12 months.
The post-doc researchers will be affiliated to the French social security system, and will be entitled to unemployment benefit at the end of the contract.
The applicants must hold a PhD. We are especially interested in candidates with background in one or several of the following fields :
linear logic (proof nets, geometry of interaction, ludics)
rewriting theory (lambda-calculus, interaction nets)
denotational semantics (category theory, games semantics, vectorial semantics)
implicit computational complexity (light logics, type systems for complexity)
Applicants should send a detailed resume by email EXCLUSIVELY, to the addresses
preferably with the subject containing the words "Complice Application" (to be sure that the application is not accidentally eaten by spam filters...).