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@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>