Title
On the Soundness of Coroutines with Snapshots.
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 Prokopec116313.56
Fengyun Liu212.39