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 lectures 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 six papers were 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 lectures 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 six papers were accepted. The special issue appeared as volume 161, 2010.

    CL&C'10

    The third meeting took place on August 21-22, 2010, in Brno, Czech Republic, organised in parallel to PECP, both in colocation with CSL and MFCS. CL&C and PECP were organised together in honour of the occasion that Helmut Schwichtenberg turned emeritus in September 2010. At the meeting, two invited lectures 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, was issued; eight papers were accepted. The special issue appeared as volume 164, 2010.

    CL&C'12

    The fourth meeting took place as a satelite to ICALP'12 on July 8, in Warwick, England. At the meeting, an invited lecture was given by P. Olivia.

    Four submitted papers were accepted as full papers, and three as short papers. The proceedings of CL&C 2012 appeared as EPTCS 97, 2012.

    CL&C'14

    The fifth meeting will take place as a satelite to LICS-CSL'14 on July 13, as part of the Summer of Logic in Vienna, Austria. At the meeting, an invited lecture will be given by Alexandre Miquel.

    The proceedings of CL&C 2014 will appear in EPTCS.