|| July 15, 2006
S. Servolo, Venice - Italy
Part of ICALP 2006
|| July 13, 2008 Reykjavik.
|| Part of ICALP 2008.
|| August 21-22 2010
|| Brno, Czech Republic.
|| Jointly with PECP. Part of MFCS & CSL 2010.
|| July 8, 2012
|| Warwick - England
|| Part of ICALP 2010.
||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
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
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
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