CL&C Congress Series
Five International Workshop on
Classical Logic and Computation

From 2006 to 2014

<< Back to the list of all CL&C congresses

CL&C06 July 15, 2006 S. Servolo, Venice - Italy Part of ICALP 2006
CL&C08 July 13, 2008 Reykjavik. Iceland Part of ICALP 2008.
CL&C10 August 21-22 2010 Brno, Czech Republic. Jointly with PECP. Part of MFCS & CSL 2010.
CL&C12 July 8, 2012 Warwick - England Part of ICALP 2010.
CL&C14 July 13, 2014 Wien - Austria Part of CSL/LICS 2014 and Floc 2014.


CL&C is a 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.

CL&C is focused on the exploration of the computational content of mathematical and logical principles. The scientific aim of this workshop is to bring together researchers from both fields and exchange ideas.

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:

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

Proceedings and Special Issues

CL&C 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.

To encourage the submission of ongoing work, at the workshop there are a session for notes or work in progress, as well as a session for accepted papers. Submissions are refereed at normal standards. CL&C recognises two kinds of papers, full (accepted) papers and short papers.

Two times the proceedings of the workshop appeared as an EPTCS Volume. Three times there was a special issue of Annals of Pure and Applied Logic including both some journal versions of papers from the congress and some new papers.

1. Annals Of Pure and Applied Logic 2008: First Special Issue dedicated to CL&C.

Steffen van Bakel, Stefano Berardi (Eds.):
Annals Of Pure and Applied Logic Volume 153, Numbers 1-3, April 2008. Special Issue: Classical Logic and Computation (2006)
  • Stéphane Lengrand, Alexandre Miquel: Classical Fomega, orthogonality and symmetric candidates. P.3-20
  • Koji Nakazawa, Makoto Tatsuta: Strong normalization of classical natural deduction with disjunctions. P.21-37
  • Kentaro Kikuchi: Call-by-name reduction and cut-elimination in classical logic. P.38-65
  • Noam Zeilberger: On the unity of duality. 66-96
  • Monika Seisenberger: Programs from proofs using classical dependent choice. P.97-110
  • Stefano Berardi, Yoriyuki Yamagata: A sequent calculus for limit computable mathematics. P.111-126
  • 2. Annals Of Pure and Applied Logic 2010: Second Special Issue dedicated to CL&C.

    Steffen van Bakel, Stefano Berardi, Ulrich Berger (Eds.):
    Ann. Pure Appl. Logic Volume 161, Number 11, August 2010. P. 1313-1314
  • Robin Adams, Zhaohui Luo: Classical predicative logic-enriched type theories. 1315-1345
  • Willem Heijltjes: Classical proof forestry. 1346-1366
  • Danko Ilik, Gyesik Lee, Hugo Herbelin: Kripke models for classical logic. 1367-1378
  • Mircea-Dan Hernest, Trifon Trifonov: Light Dialectica revisited. 1379-1389
  • Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano: Inhabitation of polymorphic and existential types. 1390-1399
  • Steffen van Bakel: Completeness and partial soundness results for intersection and union typing for lambda-mu. 1400-1430
  • 3. Proceedings CL&C 2010: EPTCS Volume 47

    Steffen van Bakel, Stefano Berardi and Ulrich Berger (Eds.):
    Proceedings Third International Workshop on Classical Logic and Computation
    (CL&C 2010, Brno).
  • Invited Presentation: Analyzing proofs based on weak sequential compactness Ulrich Kohlenbach. P. 1
  • Invited Presentation: Epsilon Substitution for Predicate Logic Grigori Mints P.3
  • Interactive Learning Based Realizability and 1-Backtracking Games Federico Aschieri P.6
  • On Various Negative Translations Gilda Ferreira and Paulo Oliva P.21
  • Superdeduction in Lambda-Bar-Mu-Mu-Tilde Clément Houtmann P.34
  • An applicative theory for FPH Reinhard Kahle and Isabel Oitavem v44
  • Relating Sequent Calculi for Bi-intuitionistic Propositional Logic Luís Pinto and Tarmo Uustalu P.57
  • Dialectica Interpretation with Marked Counterexamples Trifon Trifonov P.73
  • 4. Annals Of Pure and Applied Logic 2013: Third Special Issue dedicated to CL&C.

    Steffen van Bakel, Stefano Berardi, Ulrich Berger (Eds.)
    Preface. Ann. Pure Appl. Logic. Volume 164, Number 6, June 2013. P.589-590
  • Federico Aschieri: Learning based realizability for HA + EM1 and 1-Backtracking games: Soundness and completeness. 591-617
  • José Espírito Santo: Towards a canonical classical natural deduction system. 618-650
  • Danko Ilik: Continuation-passing style models complete for intuitionistic logic. 651-662
  • Reinhard Kahle, Isabel Oitavem: Applicative theories for the polynomial hierarchy of time and its levels. 663-675
  • Herman Geuvers, Robbert Krebbers, James McKinna: The λμT-calculus. 676-701
  • Richard McKinley: Canonical proof nets for classical logic. 702-732
  • Grigori Mints: Epsilon substitution for first- and second-order predicate logic. 733-739
  • Helmut Schwichtenberg, Christoph Senjak: Minimal from classical proofs. 740-748
  • 5. Proceedings CL&C 2012: EPTCS Volume 97

    Herman Geuvers, Ugo de'Liguoro (Eds.):
    Proceedings of the Fourth Workshop on Classical Logic and Computation
    CL&C 2012, Warwick, England, 8th July 2012. 2012 EPTCS
  • Federico Aschieri, Margherita Zorzi: Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic. P.1-18
  • Robbert Krebbers: A call-by-value lambda-calculus with lists and control.P.19-33
  • Koji Nakazawa, Shin-ya Katsumata: Extensional Models of Untyped Lambda-mu Calculus. P.35-47
  • Thomas Powell: Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma. P.49-62