基于快照的协同程序的合理性研究
On the Soundness of Coroutines with Snapshots
摘要：
协程是一种通用的控制流结构，可以消除事件驱动程序中固有的控制流碎片，并且在许多流行的语言中仍然缺失。带快照的协程是一个一流的、类型安全的、堆栈式的协程模型，它统一了许多可挂起计算的变体，并且足够通用，可以表达迭代器、单赋值变量、等待、参与者、事件流、回溯、对称协程和延续。在本文中，我们开发了一个正式的模型，称为$λ_{\rightsquigarrow}$（$λ_{\rightsquigarrow}$），捕获的本质类型安全，堆栈，定界的协程与快照。我们证明了标准的进步和保存安全性能。最后，我们展示了从$λ_{\rightsquigarrow}$演算到带引用的简单类型λ演算的形式化转换。
英文摘要：
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 $λ_{\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 $λ_{\rightsquigarrow}$ calculus to the simply-typed lambda calculus with references.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
