CL&C Home page

CL&C is a workshop 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 probably the first version (around 1917) is the following conjecture by Hilbert: "Wenn ein Existenzbeweis in der Math. geführt worden ist, so ist stets auch die Entscheidung (durch endliche Zahl von Schritten, wie man zu zagen pflegt), ob ... möglich." Translation: "If an existence theorem is once derived in the mathematics, so is always also the determination [Entscheidung] (through a finite number of steps as they are used to say), or possible." Source

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.

There are today two main lines of research. The first studies some (version of lambda) calculus adapted to represent classical logic, like the symmetric mu-calculs, or the X-calculus. The second studies semantics for programs inspired by classical proofs, like game semantic or learning algorithms. These two directions are often independent. 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).

Steering committee

  • Stefano Berardi (Turin)
  • Steffen van Bakel (Imperial College London)

    		•       CLAC logo

    CL&C'06

    The first meeting took place on July 15, 2006. The meeting was organised as a satellite to ICALP 2006 which took place in Venice, on the island of San Servolo. At the meeting, two invited lecturers were given by H. Herbelin and M. Seisenberger.

    Five submitted papers were accepted as full papers, and three were presented as short papers. The meeting was followed by general call for papers for a special issue of APAL (Annals of Pure and Applied Logic) on the topic of the workshop, for which ten papers were submitted, and six accepted. The special issue appeared as volume 153(1-3), 2008

    CL&C'08

    The second meeting took place on July 13, 2008, in Reykjavik, Iceland, in colocation with ICALP 2008. At the meeting, two invited lecturers were given by H. Schwichtenberg and S. Lengrand.

    Five submitted papers were accepted as full papers, and five were presented as short papers. The meeting was followed by general call for papers for a special issue of APAL (Annals of Pure and Applied Logic) on the topic of the workshop, for which 12 papers were submitted, and six accepted. The special issue appeared as voluem 161, 2010.

    CL&C'10

    The third meeting took place on August 21-22, 2010, in Brno, Czech Republic, in with PECP, in honour of the occasion that Helmut Schwichtenberg turned emeritus in September 2010. CL&C'10 was organised in parallel to PECP; these two workshops were organised in colocation with CSL and MFCS. At the meeting, two invited lecturers were given by H. Mints and U. Kohlenbach.

    Six submitted papers were accepted as full papers, and two were presented as short papers. The proceedings of CL&C 2010 appeared as EPTCS 47, 2010. As for previous meetings, a special issue of APAL, associated with the workshop, is being prepared, for which a general call for papers was issued; it is scheduled to appear in 2012.

    CL&C'12

    The fourth meeting will take place as a satelite to ICALP'12 on July 8, in Warwick, England; details can be found at the workshop's page