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

Structural and Computational Proof Theory

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.

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.

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

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.