Abstract | ||
---|---|---|
Coroutines are a general control flow construct that can eliminate control flow fragmentation inherent in event-driven programs, and are still missing in many popular languages. Coroutines with snapshots are a first-class, type-safe, stackful coroutine model, which unifies many variants of suspendable computing, and is sufficiently general to express iterators, single-assignment variables, async-await, actors, event streams, backtracking, symmetric coroutines and continuations. In this paper, we develop a formal model called $lambda_{rightsquigarrow}$ (lambda-squiggly) that captures the essence of type-safe, stackful, delimited coroutines with snapshots. We prove the standard progress and preservation safety properties. Finally, we show a formal transformation from the $lambda_{rightsquigarrow}$ calculus to the simply-typed lambda calculus with references. |
Year | Venue | Field |
---|---|---|
2018 | arXiv: Programming Languages | Coroutine,Lambda calculus,Programming language,Computer science,Control flow,Soundness,Backtracking,Snapshot (computer storage),Lambda |
DocType | Volume | Citations |
Journal | abs/1806.01405 | 0 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Aleksandar Prokopec | 1 | 163 | 13.56 |
Fengyun Liu | 2 | 1 | 2.39 |