Projet de Recherche — ANR Programme Blanc International 2015

FISP — The Fine Structure of Formal Proof Systems and their Computational Interpretations


Overview

FISP is carried out by a consortium of four partners, two Austrian and two French, all being internationally recognised for their work on structural proof theory, but each coming from a different tradition. One tradition originates in mathematics and is mainly concerned with first-order logic, and studies Hilbert’s epsilon calculus, Herbrand’s theorem, and Gödel’s Dialectica interpretation. A second tradition, originating in computer science, is mainly concerned with propositional systems, and studies Curry-Howard correspondence, algebraic semantics, linear logic, proof nets, and deep inference. A common ground is the role played by analytic proofs and the notion of cut-elimination.

The FISP project is part of a long-term, ambitious project whose objective is to apply the powerful and promising techniques from structural proof theory to central problems in computer science for which they have not been used before, especially the understanding of the computational content of proofs, the extraction of programs from proofs and the logical control of refined computational operations. So far, the work done in the area of computational interpretations of logical systems is mainly based on the seminal work of Gentzen, who in the mid-thirties introduced the sequent calculus and natural deduction, along with the cut-elimination procedure. But that approach reveals its limits when it comes to computational interpretations of classical logic or the modelling of parallel computing. The aim of our project, based on the complementary skills of the teams, is to overcome these limits. For instance, deep inference provides new properties, namely full symmetry and atomicity, which were not available until recently and opened new possibilities at the computing level, in the era of parallel and distributed computing.

Participating Laboratories

Université Paris Diderot
Responsible: Michel Parigot

Inria Saclay - Ile-de-France
Responsible: Lutz Straßburger

Universität Innsbruck
Responsible: Georg Moser

TU Vienna
Responsible: Matthias Baaz

Events

Open Positions

There is an open 12-month postdoc position at Inria Saclay and LIX financed by the ANR within this project.

Applicants must have a Ph.D. or equivalent in computer science or mathematics, and should have a strong background in proof theory and/or related topics.

Applications should be sent via email to Lutz Straßburger and should include a CV, a short research statement (1-2 pages), and one or two recommendation letters.

Deadline: April 16, 2017


  Last update:  March 1, 2017            Lutz Straßburger