Preface

The workshop ``Classical Logic and Computation 2008'' was held on 13 July 2008 in Reykjavik, Iceland. It was the second in a series of biennial workshops devoted to computational aspects of classical logic and mathematics. There were two invited talks, by Helmut Schwichtenberg from LMU Munich on ``Decorating Proofs'', and by Stéphane Lengrand from LIX Polytechnique on ``Inhabiting Negative Types''. The five contributed talks were by Hernest and Trifonov, ``Light Dialectica Revisited''; Hetzl, Leitsch, Weller, and Woltzenlogel Paleo, ``Herbrand Sequent Extraction''; McKinley, ``Herbrand expansion proofs and proof identity''; van Bakel, Cardelli, and Vigliotti, ``FromXto Representing the Classical Sequent Calculus in the -calculus''; and Tatsuta, Fujita, Hasegawa, and Nakano, ``Inhabitance of Existential Types is Decidable in the Negation- Product Fragment''. In addition, there were six short presentations about ongoing work. The contributions were refereed and selected by the program committee, which consisted of Paola Bruscoli (Bath), Thierry Coquand (Chalmers, Gothenburg), Fernando Ferreira (Lisbon), Michel Parigot (Paris VII), Aldo Ursini (Siena), Steffen van Bakel (Imperial College London), Stefano Berardi (Turin), and Ulrich Berger (Swansea, chair). After the workshop, there was an open call for papers for post-proceedings. The six 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 three contributions devoted to foundational questions concerning proof calculi and semantics for classical logics: Herbelin, Ilik and Lee introduce a notion of Kripke model for classical logic for which they constructively show soundness and cut-free completeness, Heijltjes proves normalization results for classical proof forests, a proof formalism for first-order classical logic based on Herbrand's Theorem and backtracking games in the style of Coquand, and van Bakel studies intersection and union type assignments for Curien's and Herbelin's Q -calculus as an investigation of type-based proof semantics. We are grateful to the Managing Editor Ulrich Kohlenbach for the handling of van Bakel's contribution. The two papers with links to type theory are by Tatsuta, Fujita, Hasegawa, and Nakano, who show that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable (using ``magic formulas''), and by Adams and Luo, who introduce two logic-enriched type theories which correspond to the classical predicative systems of second-order arithmetic, ACA0 and ACA. Practical computational issues are addressed by Hernest and Trifonov, who study an extension of Gödel's Dialectica Interpretation by ``light'' universal quantifiers which allow for a fine control of the computational content extracted from classical proofs involving the axiom of countable choice. We would like to thank the more than 30 reviewers for the time and effort they spent on scrutinizing the submitted papers. Their contributions to the scientific standard of this special issue are invaluable