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



General Information

Duration: 12 months

Starting date: Between 1 Sep 2017 and 1 Nov 2017

Working place: Inria Saclay - Ile-de-France and LIX, campus of École Polytechnique

Topic

Structural and Computational Proof Theory

Context

The postdoc position is financed by the ANR project FISP, whose objective is to investigate the fine structure of formal proof systems and their computational interpretations. Particular focus is on the computational proof theory of recent proof formalisms, like deep inference and proof nets. One of the main goals is to find canonical proof objects. 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. Another approach is the concept of focusing, which allows the design of various normal forms of proof that abstract away from many bureaucratic irrelevances.

Both concepts, proof nets and focusing, have been developped with the sequent calculus in mind. But recent results suggest that they are also suitable for deep inference formalisms, and investigating this possibility is an important part of the FISP project.

Activities for the Post Doc

The main task of the successful candidate will be to support the research effort towards the goals expressed in the scientific program of the FISP project within the Parsifal team, in particular the candidate will help in designing new proof systems that on the one hand provide canonical (i.e., bureaucracy-free) proof objects and, on the other hand, provide concrete enough structures to support computations based on proof normalization and on proof search.

Skill required

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

Application

Applicants should send their application, including CV, research statement (1-2 pages) and one or two recommendation letters to Lutz Straßburger.

Deadline: 16 April 2017



For further information, contact Lutz Straßburger.