Preface

• Published in: Annals of Pure and Applied Logic
• Main Authors: Steffen van Bakel,Stefano Berardi,Ulrich Berger, Steffen van Bakel, Stefano Berardi, Ulrich Berger
• Other Authors: BERARDI, Stefano
• Format: Other/Unknown Material
• Language: English
• Published: elsevier 2010
• Subjects: Ferreira; Chalmers; Weller; Iceland
• Online Access: http://hdl.handle.net/2318/136000; https://doi.org/10.1016/j.apal.2010.04.004; http://www.sciencedirect.com/science/article/pii/S016800721000045X

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