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

10:30 - 12:30: ESOP - Session 7 at Skeel
Chair(s): Delphine DemangeIRISA / University of Rennes 1
esop-2015-papers142917300000010:30 - 11:00
Sam LindleyUniversity of Edinburgh, J. Garrett MorrisThe University of Edinburgh
esop-2015-papers142917480000011:00 - 11:30
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford
esop-2015-papers142917660000011:30 - 12:00
Tachio TerauchiJAIST, Hiroshi UnnoUniversity of Tsukuba
esop-2015-papers142917840000012:00 - 12:30
Aws AlbarghouthiUniversity of Wisconsin - Madison, Josh BerdineMicrosoft Research, Byron CookMicrosoft Research, Zachary KincaidUniversity of Toronto