During the 2012 ASL annual meeting in Madison Wisconsin, there will be a special session on Structural Proof Theory and Computing that has been organized by Dale Miller. Several members and former members of Parsifal will present their research work during this annual meeting of the Association for Symbolic Logic.
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 and a wide range of applications to computer science. This special session will focus on recent work on structural proof theory that has applications in computing and for which computing has been, in part, an important motivation.
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
