[TYPES/announce] Control Operators and their Semantics (COS'13) - Call for Participation

Ugo de' Liguoro deligu at di.unito.it
Mon May 13 06:23:29 EDT 2013


============================================================================

      Control Operators and their Semantics (COS'13) - Call for 
Participation

                        Satellite event of RDP'13

               June 24 - 25, 2013, Eindhoven, The Nederlands

                       http://cos2013.di.unito.it/

============================================================================


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 have impact in 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 focus of the workshop 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 issue of a better understanding of control is also relevant for 
communicating
across different research areas and communities. More abstract views can 
be achieved
via several means, that include operational semantics of formal calculi, 
abstract
machines, algebraic specifications and rewriting, type assignment 
systems, denotational
semantics and game semantics, category theory and logic, to say the least.

Relevant topics include, but are not limited to:

- continuations and delimited continuations
- categorical models of continuations
- compositionality and modularity of control operators
- denotational semantics of control, event structures and causality
- operational semantics and abstract machines
- type systems for control operators
- game semantics of programming languages and of logical proofs
- usage of control operators in proof search and proof mining
- semantics of control operators in logic programming

Invited speakers:

- Mattew Flatt (Univeristy of Utah):
   Modeling a Practical Combination of Delimited Continuations,
   Exceptions, Dynamic-Wind Guards, Dynamic Binding, and Stack Inspection

- Thomas Streicher (Universitaet Darmstadt):
   A Model of Control Operators in Coherence Spaces giving rise to a new 
model of ZF


Program Committee:

Zena Ariola                 University of Oregon
Stefano Berardi             Turin University
Ken-etsu Fujita             Gunma University
Hugo Herbelin               INRIA and Laboratoire PPS (Paris 7)
Ugo de'Liguoro (co-chair)   Turin University
Koji Nakazawa               Kyoto University
Alexis Saurin (co-chair)    INRIA and Laboratoire PPS (Paris 7)

Early registration deadline is June 1. To register go to the page:

http://www.win.tue.nl/rdp2013/reg.html




More information about the Types-announce mailing list