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 Times are displayed in time zone: (GMT) Azores change
|10:30 - 11:00|
|11:00 - 11:30|
|11:30 - 12:00|
|12:00 - 12:30|