On the Soundness of Coroutines with Snapshots

TL;DR

This paper introduces a formal model for type-safe, stackful coroutines with snapshots, demonstrating their expressiveness and safety properties, and providing a transformation to standard lambda calculus.

Contribution

It presents the first formal model of type-safe, stackful coroutines with snapshots and proves their safety and expressiveness.

Findings

Proves progress and preservation safety properties.

Provides a formal transformation to simply-typed lambda calculus.

Captures a wide range of suspendable computing variants.

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.