一句话：形式化证明在简单类型 call-by-value lambda 演算中加入 ST monad 后保持纯度，并用语义类型化回译证明完全抽象。
1995 年 Launchbury 与 Peyton Jones 为 Haskell 引入 ST monad，使程序员可在封装下使用高阶可变状态，他们非形式地论证该状态计算可安全封装，不会破坏语言的纯度推理原则。本文在带递归的简单类型 call-by-value lambda 演算中加入 ST monad，形式化研究纯度的保持：证明将纯语言嵌入其 ST 扩展是完全抽象的，即纯语言的上下文等价在存在 ST 时仍成立。证明采用一种新颖技术，将目标特性（ST 计算）通过语义类型化（而非语法类型化）的回译嵌入中间语言，以应对安全编译中的经典挑战。结果已在 Coq 及 Iris 框架中完全机器化验证。
In 1995, Launchbury and Peyton Jones extended Haskell with an ST monad that allows the programmer to use higher-order mutable state. They informally argued that these state computations were safely encapsulated, and as such, that the rich reasoning principles stemming from the purity of the language, were not threatened. In this paper, we give a formal account of the preservation of purity after adding an ST monad to a simply-typed call-by-value recursive lambda calculus. We state and prove full abstraction when embedding the pure language into its extension with ST; contextual equivalences from the pure language continue to hold in the presence of ST. Proving full abstraction of compilers is usually done by emulating or back-translating the target features (here: ST computations) into the source language, a well-known challenge in the secure compilation community. We employ a novel proof technique for proving our full abstraction result that allows us to use a semantically (but not syntactically) typed back-translation into an intermediate language. We believe that this technique provides additional insight into our proof and that it is of general interest to researchers studying programming languages and compilers using full abstraction. The results presented here are fully formalized in the Coq proof assistant using the Iris framework.
@article{paperbot1522,
title = {Purity of an ST monad: full abstraction by semantically typed back-translation},
author = {Koen Jacobs and Dominique Devriese and Amin Timany},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527326}
}