ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Thu 16 Apr 2015 10:30 - 11:00 at Skeel - Session 7 Chair(s): Delphine Demange

Session types provide a static guarantee that concurrent programs respect communication protocols. Recently Caires, et al., have developed a correspondence between the propositions of linear logic and session typed pi-calculus processes. We relate the cut-elimination semantics of this approach to an operational semantics for session-typed concurrency in a functional language. We begin by presenting a variant of Wadler’s minimal session-typed functional language, GV. We give a small-step operational semantics for GV. We develop a suitable notion of deadlock for our functional setting, based on existing approaches for capturing deadlock in pi-calculus, and show that all well-typed GV programs are deadlock-free, deterministic and terminating.

Thu 16 Apr

Displayed time zone: Azores change

10:30 - 12:30
Session 7ESOP at Skeel
Chair(s): Delphine Demange IRISA / University of Rennes 1
10:30
30m
Talk
A Semantics for Propositions as Sessions
ESOP
Sam Lindley University of Edinburgh, J. Garrett Morris The University of Edinburgh
11:00
30m
Talk
Composite Replicated Data Types
ESOP
Alexey Gotsman IMDEA, Hongseok Yang University of Oxford
11:30
30m
Talk
Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
ESOP
Tachio Terauchi JAIST, Hiroshi Unno University of Tsukuba
12:00
30m
Talk
Spatial Interpolants
ESOP
Aws Albarghouthi University of Wisconsin - Madison, Josh Berdine Microsoft Research, Byron Cook Microsoft Research, Zachary Kincaid University of Toronto