Projects per year
Abstract / Description of output
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.
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.
Original language | English |
---|---|
Title of host publication | ICFP 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming |
Place of Publication | Nara, Japan |
Publisher | ACM |
Pages | 437-447 |
Number of pages | 14 |
ISBN (Print) | 978-1-4503-4219-3 |
DOIs | |
Publication status | Published - 4 Sept 2016 |
Event | 21st ACM SIGPLAN International Conference on Functional Programming - Nara, Japan Duration: 18 Sept 2016 → 24 Sept 2016 https://conf.researchr.org/home/icfp-2016 |
Publication series
Name | ACM SIGPLAN Notices |
---|---|
Publisher | ACM |
Number | 9 |
Volume | 51 |
ISSN (Print) | 0362-1340 |
ISSN (Electronic) | 1558-1160 |
Conference
Conference | 21st ACM SIGPLAN International Conference on Functional Programming |
---|---|
Abbreviated title | ICFP 2016 |
Country/Territory | Japan |
City | Nara |
Period | 18/09/16 → 24/09/16 |
Internet address |
Fingerprint
Dive into the research topics of 'Talking bananas: Structural Recursion for Session Types'. Together they form a unique fingerprint.Projects
- 1 Finished
-
From Data Types to Session Types - A Basis for Concurrency and Distribution
20/05/13 → 19/11/20
Project: Research
Profiles
-
Sam Lindley
- School of Informatics - Reader in Programming Language Design and Implementation
- Laboratory for Foundations of Computer Science
Person: Academic: Research Active