Published: 9th October 2012
DOI: 10.4204/EPTCS.97
ISSN: 2075-2180

EPTCS 97

Proceedings Fourth Workshop on
Classical Logic and Computation
Warwick, England, 8th July 2012

Edited by: Herman Geuvers and Ugo de'Liguoro
Preface
Herman Geuvers and Ugo de'Liguoro
Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic
Federico Aschieri and Margherita Zorzi		1
A call-by-value lambda-calculus with lists and control
Robbert Krebbers		19
Extensional Models of Untyped Lambda-mu Calculus
Koji Nakazawa and Shin-ya Katsumata		35
Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma
Thomas Powell		49

Preface

CL&C 2012 was the fourth of a conference series on Classical Logic and Computation, held as satellite to ICALP 2012 on Sunday July 8, 2012 in Warwick, England. CL&C intends to cover all work aiming to explore computational aspects of classical logic and mathematics, and 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. Indeed the proof theoretic analysis of non constructive theories has been widened by means of new concepts and techniques, inspired to e.g. game semantics of logic and arithmetic, as it has been illustrated in the invited lecture by Paulo Oliva, and used in contributed papers. On the other hand the theme of using control primitives such as continuations to extend functional formalisms, which is known to be related to classical reasoning since Griffin's work, is still under development and needs to be better understood, both for theoretical and practical purposes.
The intention of the organizers is for CL&C to be an informal workshop. Participants have been encouraged to present work in progress, overviews of more extensive work, and programmatic/position papers, as well as completed projects. Submission of both short abstracts and of longer papers were invited. Four submissions were accepted as full papers and are included in these proceedings. Three more were accepted only as communications for the conference. Paulo Oliva, from Queen Mary University, gave the invited talk: ''Some connections between Game Theory and Proof Theory''.

Herman Geuvers and Ugo de'Liguoro