On the Soundness of Coroutines with Snapshots

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 suspendab...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2018-06
Main Authors: Prokopec, Aleksandar, Liu, Fengyun
Format: Article
Language:English
Subjects:
Formal transformation
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422