The Fine Structure of Formal Proof Systems and their Computational Interpretations

The project The Fine Structure of Formal Proof Systems and their Computational Interpretations (FISP) forms a continuation of the STRUCTURAL project (2011-2014), whose overall aim was the application of methods of mathematical logic to computer science. FISP will focus on further developing those lines of research that have been most successful in the STRUCTURAL project. Its primary objective is the study of formal proofs and the extraction of the algorithmic content from proofs. The latter means that the implicit constructions used in a given mathematical argument can be made explicit, sometimes even fully automatically. For example it is possible to extract an algorithm fulfilling a given specification from the proof of the well-definedness of the specification. The project 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, while the other originates in computer science. A common ground is the role played by elementary proofs and proof transformations. The FISP project is part of a long-term and ambitious project whose objective is to apply the powerful and promising techniques of mathematical logic 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, work done for example 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 and distributed computing. The aim of our project, based on the complementary skills of the teams, is to overcome these limits by adapting the newest research insights for the objectives of the project. The STRUCTURAL project has demonstrated that the chosen approach and the selected lines of research are appropriate, and 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. These results illustrate 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 modelling of computational operations. Prime targets will be the logical modelling of abstract machines, as well as, parallel and distributed computations.

The Fine Structure of Formal Proof Systems and their Computational Interpretations (FISP). The aim of the FISP project can be summarised as follows. FISP investigates the fine structure of formal proofs on three intertwined levels: *) at the level of proof formalisms applicable in computing; *) at the level of logical control; *) at the level of new logical models of computing. The FISP project was 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 still 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 this 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, for example in the era of parallel and distributed computing. Main results. The now finalised FISP project has demonstrated, like the STRUCTURAL project before, that the chosen approach and the selected lines of research are appropriate, and the combined expertise of the teams led to remarkable progress in the themes of the FISP project, opening new fields of research of major interest. For example, the novel form of Miller's expansion trees with cuts have been developed; non-elementary speed-up of (locally) unsound inference rules has been studied, and studies on the lower and upper bounds of the length of Herbrand disjunctions induced by proofs coached in the epsilon calculus have been finalised. Factual informations. The FISP project was an international basic research project coordinated by Michel Parigot (University Paris-Diderot). It brings together teams of (i) the University of Innsbruck, (ii) the Vienna University of Technology, (iii) INRIA Saclay, and (iv) the University University Paris-Diderot. The Austrian side of the project has been coordinated by Georg Moser (University of Innsbruck). The project started on January, 1 2016 and lasted 42 months. It benefited from an FWF funding of EUR 310.842,-.