Duration: 12 month

Starting date: Between 1 Oct 2009 and 1 Dec 2009

Working place: École
Polytechnique, LIX

Canonical proof systems

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.

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.

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

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.