April 2--April 3, 2012, Madison, Wisconsin

held during the 2012 ASL annual meeting

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.

- Dale Miller, An overview of Structural Proof Theory and Computing
- Alexis Saurin, Proof search and the logic of interaction
- David Baelde, A proof theoretical journey from programming to model checking and theorem proving
- Stefan Hetzl, Which proofs can be computed by cut-elimination?
- Marco Gaboardi, Light Logics for Polynomial Time Computations

INRIA Saclay and LIX/Ecole Polytechnique, Palaiseau, France

**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**.

ITU Copenhagen, Denmark

**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**.

Vienna University of Technology, Austria

**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**.

University of Pennsylvania, USA

**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**.

PPS, Univ of Paris 7, France

**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.