Published: 4th September 2013
DOI: 10.4204/EPTCS.127
ISSN: 2075-2180

EPTCS 127

Proceedings First Workshop on
Control Operators and their Semantics
Eindhoven, The Netherlands, June 24-25, 2013

Edited by: Ugo de'Liguoro and Alexis Saurin
Preface
Ugo de'Liguoro and Alexis Saurin
Strong Normalization for HA + EM1 by Non-Deterministic Choice
Federico Aschieri		1
Proving termination of evaluation for System F with control operators
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet and Marek Materzok		15
Interpreting a Classical Geometric Proof with Interactive Realizability
Giovanni Birolo		30
Hereditary Substitution for the λΔ-Calculus
Harley Eades and Aaron Stump		45
Continuation calculus
Bram Geron and Herman Geuvers		66
Type Directed Partial Evaluation for Level-1 Shift and Reset
Danko Ilik		86
Induction by Coinduction and Control Operators in Call-by-Name
Yoshihiko Kakutani and Daisuke Kimura		101
Combining and Relating Control Effects and their Semantics
James Laird		113

Preface

The first workshop on "Control Operators and their Semantics" was held in Eindhoven on the 24th and 25th of June 2013, affiliated with the seventh International Conference on Rewriting, Deduction, and Programming (RDP 2013). The aim of the workshop was to address the issue of control in programming both from a logical and programming languages perspective. Modern programming languages provide sophisticated control mechanisms, commonly referred to as control operators which are widely used to realize a variety of applications. Since we cannot escape control features, it becomes a challenge to provide them with sound reasoning principles. There is a very active research on understanding, manipulating, representing, and reasoning about elaborated non-local control structures, in particular in declarative programming languages such as functional and logic languages. Ideas and results originating from this research area impact many other areas of computer science, like distributed and concurrent systems, proof theory, proof mining, web programming and linguistics. For instance, the study of the logical foundations of control operators renewed the study of the connections between proofs and programs via the so-called Curry-Howard correspondence, providing new methods to extract the computational content of classical proofs.

The program committee of COS 2013 consisted in:

The focus of the papers presented in this volume is on the interplay between syntax and semantics, namely the central question of what a program means and how it does define the intended procedure. This is a crucial issue especially in the case of control operators, since they are as powerful as potentially obscure, and programs that use them are usually more error-prone than purely declarative ones. The included contributions provide perspectives on the topic of control operators via operational semantics of formal calculi as well as type assignment systems, denotational semantics, game semantics, category theory and logic. In addition to the contributed papers, COS received two invited talks: Modeling a Practical Combination of Delimited Continuations, Exceptions by Matthew Flatt from the University of Utah and A Model of Control Operators in Coherence Spaces giving rise to a new model of ZF by Thomas Streicher from Darmstadt University.
24th of July, 2013 Ugo de'Liguoro
Alexis Saurin