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).
      CLAC logo

CL&C'06

The first meeting took place on July 15, 2006. The meeting was organised as a satelite 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 10 papers were submitted, and six accepted. The special issue will appear in 2008.

CL&C'08

The second meeting will take place on July 13, 2008, in Reykjavik, Iceland, in colocation with ICALP 2008. The call for papers can be found here.

Important dates

Programme committee

Invited speakers