CL&C'06
First International Workshop on
Classical Logic and Computation
July 15, 2006 S. Servolo, Venice - Italy

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

Scope

CL&C'06 is the first of a new conference series on "Classical Logic and Computation". It intends to cover all work aiming to propose a programming language inspired by classical logic, and a semantics for it.

The fact that classical mathematical proofs of simply existential statements can be read as programs was established by Godel and Kreisel some 50 years ago. But the possibility of programming using a style inspired by Classical Logic (much as functional programming is inspired by Intuitionistic Logic) was taken seriously only after the seminal work of Griffin about typing continuations.

There are today two main lines of research. The first studies some (version of lambda) calculus adapted to represent classical logic, like the symmetric mu-calculs, or the X-calculus. The second studies semantics for programs inspired by classical proofs, like game semantic or learning algorithms. These two directions are often independent. This workshop aims to start a fruitful exchange of ideas in the field.

CL&C'06 is part of ICALP 2006.

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 outlining what will be presented at the workshop and of longer papers describing completed work, either published or unpublished, in the following areas:

  • types for lambda calculus with continuations
  • design of programming languages inspired by classical logic,
  • witness extraction from classical proofs,
  • constructive semantic for classical logic (e.g. game semantic),
  • case studies (for any of the previous points)

In order to make a submission:

Submissions will be refereed at normal standards. A participants' proceedings will be distributed at the workshop. A special issue of APAL associated with the workshop is being considered; this will be discussed at the workshop.

Important dates

  • Deadline for submission: April, 14.
  • Notification of acceptance: May, 15.
  • Final version due: June, 25.
  • Workshop date: July 15.

    • Accepted papers are:

  • Stéphane Lengrand, University of St Andrews & PPS, Alexandre Miquel, PPS & University Paris 7 A classical version of system F-omega
  • Yevgeniy Makarov, Indiana University Simplifying Programs Extracted from Classical Proofs
  • Kentaro Kikuchi, RIEC, Tohoku University Call-by-Name Reduction and Cut-Elimination in Classical Logic
  • Stefano Berardi, C.S. Dept. ,Univ. of Turin Yoriyuki Yamagata, National Institute of Advanced Industrial Science and Technology A sequent calculus for Limit Computable Mathematics

    Revise:

  • Lutz Strassburger, INRIA Futurs What is a Boolean Category ?
  • Robert Meyer, CSL, Australian National University Types, Relevance & Classical Logic

    • Short paper / note

  • Silvia Likavec, Universita di Torino, Italy Pierre Lescanne, ENS Lyon, France On untyped Curien-Herbelin calculus
  • Christian Urban, Technical University of Munich Diana Ratiu, University of Munich Classical Logic is better than Intuitionistic Logic: A Conjecture about Double-Negation Translations

    APAL Special Issue for CL&C06: go back to list of all CL&C congresses

    		• CLAC logo

    Programme committee

  • Steffen van Bakel (Imperial College London): co-chair
  • Stefano Berardi (Turin): co-chair
  • Ulrich Berger (Swansea)
  • Theirry Coquand (Chalmers)
  • Pierre-Louis Curien (Paris VII)
  • Roy Dyckhoff (St Andrews)
  • Herman Geuvers (Nijmegen)
  • Hugo Herbelin (Inria)
  • Luke Ong (Oxford)
  • Michel Parigot (Paris VII)
  • Helmut Schwichtenberg (Muenchen)
  • Philip Wadler (Edinburgh)