Preface

The workshop “Classical Logic and Computation 2010 (CLAC 2010)” was held on the 22nd of August 2010 in Brno, Czech Republic. It was the third in a series of biennial workshops devoted to computational aspects of classical logic and mathematics. In 2010 it was held in conjunction with the workshop “Program Extraction and Constructive Proofs (PECP 2010)” and colocated with MFPS and CSL. CLAC 2010 and PECP 2010 were dedicated to Helmut Schwichtenberg on the occasion of his retirement to honor his many important contributions to the fields of both workshops. The five joint invited talks of CLAC 2010 and PECP 2010 were by Ulrich Kohlenbach (Darmstadt) on “Analyzing proofs based on weak sequential compactness”, Grigori Mints (Stanford) on “Epsilon substitution in predicate logic”, Michael Rathjen (Leeds) on “Finding witnesses for existential theorems in intuitionistic set theories”, Helmut Schwichtenberg (Munich) on “Proofs and Computations”, and Stan Wainer (Leeds) on “A Hierarchy of “Predicative” Theories within PRA”. CLAC 2010 had eight contributed talks: Frederico Aschieri, Interactive learning based realizability and 1-backtracking games; Gilda Ferreira and Paulo Oliva, On various negative translations; Stefan Hetzl, Alexander Leitsch and Daniel Weller, CERES in higher-order logic; Clement Houtman, Superdeduction in ¯ λμ˜μ; Reinhard Kahle and Isabel Oitavem, An applicative theory for PH; Luis Pinto and Tarmo Uustalu, Relating sequent calculi for bi-intuitistic propositional logic; Trifon Trifonov, Dialectica interpretation with marked counterexamples; Jeffrey Vaughan, A logical interpretation of Java-style exceptions. The contributions were refereed and selected by the programme committee which consisted of Hugo Herbelin (INRIA, Paris), Zhaohui Luo (Royal Holloway, London), Richard Mckinley (Berne), Ugo De Liguoro (Turin), Stephane Lengrand (CNRS, Palaiseau), Bernhard Reus (Sussex), Steffen van Bakel (Imperial College, London), Stefano Berardi (Turin), and Ulrich Berger (Swansea, chair). After the conference, there was an open call for papers for post-proceedings. The eight papers that were accepted are the content of this special issue. They represent a good deal of the current research on classical logic and computation covering foundational, type theoretic and practical aspects. There are two contributions studying the computational content of classical systems. Federico Aschieri proves a soundness and completeness result for learning based realizability for Heyting Arithmetic plus Excluded Middle over semidecidable statements with respect to 1-Backtracking and game semantics. Reinhard Kahle and Isabel Oitavem study classical applicative theories for the polynomial hierarchy of time and its levels. The second group of papers is devoted to variations of Parigot’s λμ-calculus. Jose Espirito Santo introduces the λμletcalculus as a canonical classical natural deduction system. Herman Geuvers, Robbert Krebbers and James Mckinna combine the λμ-calculus with Gödel’s system T to the λT μ-calculus and prove that this system is confluent and strongly normalizing. The semantics of classical and intuitionistic logic is the topic of the third group of papers. Richard Mckinley studies canonical proof-nets for propositional classical logic. Danko Ilik investigates continuation-passing style models which are complete for intuitionistic logic. The last group of contributions deals with classical problems in logic. Grigori Mints reviews Hilbert’s epsilon substitution method for first- and second-order predicate logic and suggests ways to tackle the open problem of termination for the second-order case. Helmut Schwichtenberg and Christoph Senjak prove that for