Published: 9th September 2014|
|Preface Paulo Oliva|
|A type system for Continuation Calculus Herman Geuvers, Wouter Geraedts, Bram Geron and Judith van Stegeren||1|
|A Sheaf Model of the Algebraic Closure Bassel Mannaa and Thierry Coquand||18|
|A fully-abstract semantics of lambda-mu in the pi-calculus Steffen van Bakel and Maria Grazia Vigliotti||33|
|Infinitary Classical Logic: Recursive Equations and Interactive Semantics Michele Basaldella||48|
|Confluence for classical logic through the distinction between values and computations José Espírito Santo, Ralph Matthes, Koji Nakazawa and Luís Pinto||63|
|A proof-theoretic view on scheduling in concurrency Emmanuel Beffara||78|
The fact that classical mathematical proofs of simply existential statements can be read as programs was established by Gödel and Kreisel more than 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 Gödel'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.
Classical Logic and Computation (CL&C) 2014 is the fifth edition of this workshop series. The workshop series intends to cover all work aiming to explore computational aspects of classical logic and mathematics. Its focus is on the exploration of the computational content of mathematical and logical principles. The scientific aim of this workshop series is to bring together researchers from both fields and exchange ideas.
In this fifth edition we received 18 submissions of both short and full papers. Fourteen (14) of these were selected to present at the meeting in Vienna, and six (6) full papers were accepted to appear at this ETPCS special volume. Topics covered by this years submissions included: translations of classical to intuitionistic proofs, witness extraction from classical proofs, confluence properties for classical systems, linear logic, constructive semantics for classical logic (game semantics, realizability), and the study of calculi based on classical logic (lambda-mu-calculus, continuation calculus).
Finally, I would like to thank the members of programme committee for their excellent work:
Paulo Oliva (PC Chair)