Call for a post-doc position at INRIA Saclay—Ile-de-France

General Information

Duration: 12 month

Starting date: Between 1 Oct 2009 and 1 Dec 2009

Working place: École Polytechnique, LIX


Canonical proof systems

Research Context

Traditional proof systems, like sequent calculus, tableaux, or resolution do not provide canonical proofs. The reason is that their syntax allows for many irrelevant rule permutation. Proof nets have been conceived to abstract away from these rule permutation, and thus form a "bureaucracy-free" approach to encoding proofs. But the lack of explicit structure in proof nets makes algorithmic aspects of proofs difficult to describe when the logic reaches a certain expressive power. In other words, they are not suited for proof search. It is an important research problem to design new proof systems that on the one hand provide canonical (i.e., bureaucracy-free) proof objects, and on the other hand provide a rich enough structure for performing proof search.

Activities for the Post Doc

The main task of the successful candidate will be to support the recent research effort within the Parsifal team, in particular the work on focused proofs and proof nets. Concurrently, members of Parsifal have been pushing the notion of "focused proof" to its limit and obtained a "maximally multi-focused" proof system, which yields canonical proof objects for multiplicative additive linear logic without units. It is now important to exhibit the precise relation to proof nets and to see how this can be extended to other logics, in particular, classical logic.

Skill required

The candidate should have a good background in proof theory and related fields.


Applicants should send their application (CV and recommendation letters) to Lutz Straßburger.

Deadline: 30 April 2009

Further particulars

The position is part of the ARC Redo.

It an INRIA-postdoc position. That means that the candidate must fulfill the formal requirements for INRIA postdocs which can be found at INRIA's web-page. In particular, the candidate must have held a doctorate or Ph.D. for less than one year before the recruitment date. If the Ph.D. is not defended at the application date, you should cleary point out the defence date and the composition of jury.

The salary is 2357.30 euros gross per month.

The application process for this position is independent from the INRIA-postdoc campaign.

For further information, contact Lutz Straßburger.