Proceedings Third International Workshop on Classical Logic and Computation

TL;DR

This collection of papers from a 2010 workshop explores the computational content of classical logic proofs, including proof interpretations, calculi, and applications in algorithms and complexity theory.

Contribution

It presents recent advances in proof interpretations and computational methods for classical logic, extending the Curry-Howard correspondence and exploring proof optimization techniques.

Findings

Proof interpretations can yield new algorithms and numerical results.

Extensions of Curry-Howard correspondence to classical logic are feasible.

Various calculi and theories capture computational and complexity aspects of classical logic.

Abstract

The fact that classical mathematical proofs of simply existential statements can be read as programs was established by Goedel and Kreisel half a century ago. But the possibility of extracting useful computational content from classical proofs was taken seriously only from the 1990s on when it was discovered that proof interpretations based on Goedel's and Kreisel's ideas can provide new nontrivial algorithms and numerical results, and the Curry-Howard correspondence can be extended to classical logic via programming concepts such as continuations and control operators. The workshop series "Classical Logic and Computation" aims to support a fruitful exchange of ideas between the various lines of research on computational aspects of classical logic. This volume contains the abstracts of the invited lectures and the accepted contributed papers of the third CL&C workshop which was held jointly with the workshop "Program Extraction and Constructive Mathematics" at the University of Brno in August 21-22, 2010, as a satellite of CSL and MFCS. The workshops were held in honour of Helmut Schwichtenberg who became "professor emeritus" in September 2010. The topics of the papers include the foundations, optimizations and applications of proof interpretations such as Hilbert's epsilon substitution method, Goedel's functional interpretation, learning based realizability and negative translations as well as special calculi and theories capturing computational and complexity-theoretic aspects of classical logic such as the lambda-mu-calculus, applicative theories, sequent-calculi, resolution and cut-elimination