Fourth International Workshop on
Classical Logic and Computation

July 8, 2012, Warwick - England

<< Go back to list of all CL&C congresses


CL&C'12 is the fourth of 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).

Submission and Publication

This 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 will be a session for notes or work in progress, as well as a session for accepted papers. In order to make a submission:

Submissions will be refereed at normal standards. CL&C recognises two kinds of papers, full (accepted) papers and short papers; the full papers will apear in EPTCS.

CL&C'12 is part of ICALP'12.

CL&C 2012 Program - Sunday 8 July 2012

  • 10:00 - 10:45 K. Nakazawa, S. Katsumata: "Extensional Models of Untyped Lambda-Mu Calculus"
  • 10:45 - 11:15 Coffee break
  • 11:15 - 12.00 F. Aschieri, M. Zorzi: "Eliminating Skolem functions in Peano Arithmetic with Interactive Realizability"
  • 12.00 - 12.20 H. Eades: "Hereditary Substitution for the Lambda-Mu Calculus" (short communication)
  • 12.20 - 12.40 G. Birolo: "A simple geometric example of Interactive Realizability" (short communication)
  • 12:40 - 14:00 Lunch
  • 14:00 - 15:00 P. Oliva "Some connections between Game Theory and Proof Theory" (invited talk)
  • 15:00 - 15:45 R. Krebbers: "A call-by-value lambda-calculus with lists and control"
  • 15:45 - 16:15 Coffee break
  • 16:15 – 17.00 T. Powel: "Applying Goedel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma"
  • 17.00 - 17:20 S. Sanders: "Nonstandard Analysis: a New Way to Compute (Constructively)" (short communication)
  • 17.20 closure of the workshop

    EPTCS Proceedings: Go back to list of all CL&C congresses

  • Important dates

  • Deadline for paper submission: April 23, 2012. (new)
  • Notification of acceptance: June 18, 2012. (new)
  • Final version due: June 28, 2012. (new)
  • Workshop date: July 8, 2012.
  • Programme committee

  • Herman Geuvers (Nijmegen) - chair
  • Silvia Ghilezan (Novi Sad)
  • Stefano Berardi (Turin)
  • Steffen van Bakel (Imperial College London)
  • Koji Nakazawa (Kyoto)
  • Ugo de'Liguoro (Turin)
  • Steering committee

  • Stefano Berardi (Turin)
  • Steffen van Bakel (Imperial College London)
  • CLAC logo