[TYPES/announce] post-doc position in proof theory at INRIA Saclay (Paris)

[lutz@lix.polytechnique.fr]

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

Duration: 12 month
Starting date: Between 1 Oct 2009 and 1 Dec 2009
Working place: Ecole Polytechnique, LIX, Equipe Parsifal

Topic:
------

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.


Application:
------------

Applicants should send their application to Lutz Strassburger
<lutz at lix.polytechnique.fr> before 30 April 2009.


Further particulars:
--------------------

The position is part of the "INRIA Action de Recherche Collaborative"
REDO: <http://www.lix.polytechnique.fr/~lutz/orgs/redo.html>

The position is an INRIA-postdoc position. That means that the
candidate must fulfill the formal requirements for INRIA postdocs
which can be found at the web-page
<http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html>

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.

Further details:
<http://www.lix.polytechnique.fr/~lutz/orgs/arc-postdoc.html>