Second International Workshop on
Classical Logic and Computation

Sunday, July 13, 2008 Reykjavik, Iceland

<< Go back to list of all CL&C congresses


CL&C'08 is the second of a new conference series on "Classical Logic and Computation". It intends to cover all work aiming to explore computational aspects of classical logic and mathematics.

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.

This workshop aims to support a fruitful exchange of ideas between the various lines of research on Classical Logic and Computation. Topics of interest include, but are not limited to:

  • version of lambda calculi adapted to represent classical logic,
  • design of programming languages inspired by classical logic,
  • cut-elimination for classical systems,
  • proof representation and proof search for classical logic,
  • translations of classical to intuitionistic proofs,
  • constructive interpretation of non-constructive principles,
  • witness extraction from classical proofs,
  • constructive semantics for classical logic (e.g. game semantics),
  • case studies (for any of the previous points).

Submission and Publication

This is intended to be an informal workshop. Participants are encouraged to present work in progress, overviews of more extensive work, and programmatic/position papers, as well as completed projects. We therefore ask for submission both of short abstracts and of longer papers. In order to make a submission:

Submissions will be refereed at normal standards. A participants' proceedings will be distributed at the workshop. A special issue of a journal, associated with the workshop, is being considered. It will contain full versions of selected papers.

Important dates

  • Deadline for submission: April 11, 2008.
  • Notification of acceptance: May 22, 2008.
  • Final version due: June 23 2008.
  • Workshop date: July 13, 2008.

CL&C'08 is part of ICALP 2008.

Accepted papers

Dan Hernest and Trifon Trifonov Light Dialectica Revisited
Stefan Hetzl, Alexander Leitsch, Daniel Weller and Bruno Woltzenlogel Paleo Herbrand Sequent Extraction
Richard McKinley Herbrand expansion proofs and proof identity
Makoto Tatsuta, Ken-etsu Fujita,
Ryu Hasegawa and Hiroshi Nakano
Inhabitance of Existential Types is Decidable in Negation-Product Fragment
Steffen van Bakel, Luca Cardelli and
Maria Grazia Vigliotti
From X to pi; Representing the Classical Sequent Calculus in the Pi-calculus

Short paper / note

James Brotherston and Cristiano Calcagno Classical Logic of Bunched Implications
Ozan Kahramanogullari Ingredients of a Deep Inference Theorem Prover
Diana Ratiu An Application of the Refined A-Translation for a Variant of the Infinite Pigeon Hole Principle
Alexander Summers A Curry-Howard Correspondence for a Canonical Classical Natural Deduction
Willem Heijltjes Proof Forests with Cut-Elimination Based on Herbrand's Theorem

EPTCS Proceedings and APAL Special Issue for CL&C08: go back to list of all CL&C congresses

Programme committee

  • Steffen van Bakel (Imperial College London)
  • Stefano Berardi (Turin)
  • Ulrich Berger (Swansea): chair
  • Paola Bruscoli (Bath)
  • Thierry Coquand (Chalmers)
  • Fernando Ferreira (Lisbon)
  • Michel Parigot (Paris VII)
  • Aldo Ursini (Siena)
  • Invited speakers

  • Helmut Schwichtenberg (München)
  • Stéphane Lengrand (LIX Polytechnique)
  • CLAC logo