一句话：把 Dijkstra 单子框架扩展到交互树，为带代数效应的非终止交互式程序提供终止敏感的规约与验证。
Dijkstra 单子框架可以让程序员用单子效应为带副作用的程序书写规约，但原有形式无法描述非终止的、与外部环境交互的程序。本文引入面向“带未解释事件的非终止程序”的基础规约单子，从而把终止性纳入规约语义之中。程序本身用 interaction trees 建模——这是 Coq 中表示带代数效应程序的余归纳数据类型；作者进一步为它补充 trace 语义，使规约可以谈论交互过程中产生的可观察事件轨迹。作者论证该框架可以涵盖若干常见的、直接的证明原则，说明其表达力足以支撑实际推理。整个框架作为 Interaction Trees Coq 库的扩展实现，提供机器化验证支持。
This paper extends the Dijkstra monad framework, designed for writing specifications over effectful programs using monadic effects, to handle termination sensitive specifications over interactive programs. We achieve this by introducing base specification monads for non-terminating programs with uninterpreted events. We model such programs using interaction trees, a coinductive datatype for representing programs with algebraic effects in Coq, which we further develop by adding trace semantics. We show that this approach subsumes typical, simple proof principles. The framework is implemented as an extension of the Interaction Trees Coq library.
@article{paperbot1185,
title = {Dijkstra monads forever: termination-sensitive specifications for interaction trees},
author = {Lucas Silver and Steve Zdancewic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434307}
}