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 2122 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.

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 CurryHoward 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,
 cutelimination for classical systems,
 proof representation and proof search for classical logic,
 translations of classical to intuitionistic proofs,
 constructive interpretation of nonconstructive 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 13, April 2008.
Special Issue: Classical Logic and Computation (2006)
Stéphane Lengrand, Alexandre Miquel: Classical Fomega, orthogonality and symmetric candidates. P.320
Koji Nakazawa, Makoto Tatsuta: Strong normalization of classical natural deduction with disjunctions. P.2137
Kentaro Kikuchi: Callbyname reduction and cutelimination in classical logic. P.3865
Noam Zeilberger: On the unity of duality. 6696
Monika Seisenberger: Programs from proofs using classical dependent choice. P.97110
Stefano Berardi, Yoriyuki Yamagata: A sequent calculus for limit computable mathematics. P.111126

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. 13131314
Robin Adams, Zhaohui Luo: Classical predicative logicenriched type theories. 13151345
Willem Heijltjes: Classical proof forestry. 13461366
Danko Ilik, Gyesik Lee, Hugo Herbelin: Kripke models for classical logic. 13671378
MirceaDan Hernest, Trifon Trifonov: Light Dialectica revisited. 13791389
Makoto Tatsuta, Kenetsu Fujita, Ryu Hasegawa, Hiroshi Nakano: Inhabitation of polymorphic and existential types. 13901399
Steffen van Bakel: Completeness and partial soundness results for intersection and union typing for lambdamu. 14001430

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 1Backtracking Games
Federico Aschieri P.6
On Various Negative Translations
Gilda Ferreira and Paulo Oliva P.21
Superdeduction in LambdaBarMuMuTilde
Clément Houtmann P.34
An applicative theory for FPH
Reinhard Kahle and Isabel Oitavem v44
Relating Sequent Calculi for Biintuitionistic 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.589590
Federico Aschieri: Learning based realizability for HA + EM1 and 1Backtracking games: Soundness and completeness. 591617
José Espírito Santo: Towards a canonical classical natural deduction system. 618650
Danko Ilik: Continuationpassing style models complete for intuitionistic logic. 651662
Reinhard Kahle, Isabel Oitavem: Applicative theories for the polynomial hierarchy of time and its levels. 663675
Herman Geuvers, Robbert Krebbers, James McKinna: The λμTcalculus. 676701
Richard McKinley: Canonical proof nets for classical logic. 702732
Grigori Mints: Epsilon substitution for first and secondorder predicate logic. 733739
Helmut Schwichtenberg, Christoph Senjak: Minimal from classical proofs. 740748

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.118
Robbert Krebbers: A callbyvalue lambdacalculus with lists and control.P.1933
Koji Nakazawa, Shinya Katsumata: Extensional Models of Untyped Lambdamu Calculus. P.3547
Thomas Powell: Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma. P.4962

