Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Wed 21 Sep 2016 15:05 - 15:30 at Noh Theater - Session 11 Chair(s): Alejandro Russo

Session types provide static guarantees that concurrent programs respect communication protocols. We give a novel account of recursive session types in the context of GV, a small concurrent extension of the linear λ-calculus. We extend GV with recursive types and catamorphisms, following the initial algebra semantics of recursion, and show that doing so naturally gives rise to recursive session types. We show that this principled approach to recursion resolves long-standing problems in the treatment of duality for recursive session types.

We characterize the expressiveness of GV concurrency by giving a CPS translation to (non-concurrent) λ-calculus and proving that reduction in GV is simulated by full reduction in λ-calculus. This shows that GV remains terminating in the presence of positive recursive types, and that such arguments extend to other extensions of GV, such as polymorphism or non-linear types, by appeal to normalization results for sequential λ-calculi. We also show that GV remains deadlock free and deterministic in the presence of recursive types.

Finally, we extend CP, a session-typed process calculus based on linear logic, with recursive types, and show that doing so preserves the connection between reduction in GV and cut elimination in CP.

Wed 21 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

15:05 - 16:20
Session 11Research Papers at Noh Theater
Chair(s): Alejandro Russo Chalmers University of Technology
15:05
25m
Talk
Talking Bananas: Structural Recursion for Session Types
Research Papers
Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Edinburgh, UK
DOI
15:30
25m
Talk
The Best of Both Worlds: Linear Functional Programming without Compromise
Research Papers
J. Garrett Morris University of Edinburgh, UK
DOI
15:55
25m
Talk
Context-Free Session Types
Research Papers
Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos INESC-ID / Instituto Superior Técnico, Universidade de Lisboa
DOI