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

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