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

Scope

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