The study of the structural properties of proofs has evolved a great deal since Gentzen's original proof of cut-elimination for classical and intuitionistic sequent calculus proofs. The recent 20-30 years has seen an explosion of results in the area of Structural Proof Theory that have brought us linear logic as well as a wide range of applications to computer science.
This special session focused on recent work in structural proof theory that has applications in computing and for which computing has been, in part, an important motivation.
This session took place on 3 April 2012. All talks in this session were 35 minutes long. The official program for the full conference can be found here.
This session includes the following speakers.
Abstract: Structural Proof Theory organizes the presentation of proofs around analytic methods. This field was started with Gentzen when he introduced the LJ and LK sequent calculus proofs systems for intuitionistic and classical logics and significantly strengthen by Girard's introduction of linear logic. This talk will provide an overview of keys ways in which structural proof theory can be used to describe and reason about computing. The description of functional programming using the Curry-Howard correspondence and proof-normalization is familiar to most researchers. We shall also describe how the search for proofs can also be seen as computing and that this framework for presenting computation naturally describes logic programming. The key role of the cut-elimination theorem and the completeness of focused proofs systems will also be illustrated. Slides.
Abstract: In this talk, we will go through increasingly demanding tasks involving logic. All the way long, focusing provides crucial structure which tightens the connection between logic and computation. Starting from logic programming, we'll see how fixed points bring a more faithful logical account of logic programs, and thus more reasoning capabilities. This will bring general theorem proving capabilities, and some insights on automating it. In between logic programming and theorem proving, we'll encounter model-checking, and some very nice results relating proof theory and automata theory. Slides.
Abstract: In classical logic, it is typically possible to compute significantly different cut-free proofs from a single proof with cuts using a non-deterministic algorithm like Gentzen's procedure based on local proof rewriting steps. I will first speak about results that support this point by relating the number of cut-free proofs thus obtainable to the functions provably total in the system under consideration. Then I will turn towards recent work on characterizing the cut-free proofs induced by a given proof with cuts. Slides.
Abstract: I overview the Linear Logic approach to Implicit Computational Complexity. I present two different logical systems characterizing the class of polynomial time functions by restricting structural rules. I then point out some results obtained using extensions and generalizations of these structural principles and their use to prove properties of functional programs. Slides.
Abstract: Proof theory deeply impacted two main paradigms of declarative programming languages, namely logic programming and functional programming. This influenced the design of programming languages as well as the analysis of program behaviors: the most striking example of this interplay is probably the Curry-Howard correspondence unveiled 40 years ago.
Considering the aforementioned connections between logic and programming, one may expect that a better understanding of the essence of proofs will provide more sophisticated tools for analyzing programs. Ludics has been introduced in 1999 by J-Y Girard, building on research undertaken in the previous two decades on linear logic, the geometry of interaction as well as game-theoretical interpretation of logic and programming languages. Ludics can be described as a reconstruction of logic from the concept of interaction.
After providing background on this interactive approach, I will explain how the interactive approach to logic and proof theory suggests new directions for computation as proof-search.