DS0705 - Sciences et technologies logicielles

The fine structure of formal proof systems and their computational interpretations – FISP

Submission summary

The FISP project fits in the continuation of the STRUCTURAL project (2011-2013), whose overall aim was to investigate the structure of formal proofs and the associated computational interpretations. FISP will focus on further developing the lines of research that have proved most fruitful in the STRUCTURAL project. Its primary objective is to build new concrete computational interpretations of proof systems based on these techniques.

The project is carried out by a consortium of four partners, two Austrian and two French, all being internationally recognized for their work on structural proof theory, but each coming from a different tradition. One tradition comes from 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 comes from 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 Gentzen’s seminal work, which in the mid-thirties introduced the sequent calculus and natural deduction and the cut-elimination procedure. But that approach shows its limits when it comes to computational interpretations of classical logic or modeling 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.

The STRUCTURAL project has shown that the chosen approach and the selected lines of research are appropriate, and that the combined expertise of the teams led to remarkable progress in three themes of the FISP project, opening new fields of research of major interest. For example, it has been shown that computational interpretations of Deep Inference can provide an adequate typing for the lambda-calculus with explicit sharing and also for interaction nets. It has also been shown that, surprisingly, the non determinism of the computational interpretations of classical logic can be controlled by Herbrand formulas.

These results show the great potential and relevance of the chosen techniques. The objective of the FISP project will be to continue the theoretical development of these techniques and to provide new applications in terms of logical modeling of computational operations. Prime targets will be the logical modeling of abstract machines and parallel and distributed computations.

Project coordinator

Monsieur Michel Parigot (Université Paris Diderot / Laboratoire Preuves, programmes, systèmes (PPS))

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

Université Paris Diderot / PPS Université Paris Diderot / Laboratoire Preuves, programmes, systèmes (PPS)
Inria Saclay - Ile-de-France/Equipe proj Inria - Centre de recherche Saclay - Ile-de-France/ Equipe projet PARSIFAL
Universtität Innsbruck Universtität Innsbruck / Computationale Logik
Technische Universität Wien Technische Universität Wien / Institut für Diskrete Mathematik und Geometrie

Help of the ANR 316,805 euros
Beginning and duration of the scientific project: December 2015 - 36 Months

Useful links