关于带快照协程的可靠性

协程是一种通用的控制流构造，可以消除事件驱动程序中固有的控制流碎片化，但在许多流行语言中仍然缺失。带快照的协程是一种一等、类型安全、有栈的协程模型，它统一了可挂起计算的多种变体，并且足够通用以表达迭代器、单赋值变量、async-await、actor、事件流、回溯、对称协程和续延。在本文中，我们开发了一个称为 $\lambda_{\rightsquigarrow}$（lambda-squiggly）的形式化模型，该模型捕捉了带快照的类型安全、有栈、定界协程的本质。我们证明了标准的进展性和保持性安全性质。最后，我们展示了从 $\lambda_{\rightsquigarrow}$ 演算到带引用的简单类型 lambda 演算的形式化变换。