一句话：提出交互树，在 Coq 中表示递归、有副作用且可能非终止的程序，支持组合解释与弱互模拟等式推理。
本文提出交互树（ITrees），一种在 Coq 中表示与环境交互的递归程序行为的通用数据结构。ITrees 可视为共归纳的“自由单子”，由未解释事件及其续延构成，支持从事件处理器组合式构造解释器，并具有弱互模拟下的丰富等式理论。它能表达不纯、可能非终止和互递归的计算，又可通过代码抽取执行。作者在 Coq 中实现 ITrees 及相关理论，机械化了程序语义、迭代、单子结构与等式推理中的经典结果；库内部大量使用共归纳证明，但接口隐藏细节。为展示效用，他们证明从简单命令式源语言到类汇编目标的编译器的终止敏感正确性，目标语言意义由基于 ITree 的指称语义给出；互模拟证明通过结构归纳和控制流图组合子的等式重写完成。
Interaction trees (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of “free monads,” ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers , which give meaning to events by defining their semantics as monadic actions. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification. We have implemented ITrees and their associated theory as a Coq library, mechanizing classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library rely heavily on coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq’s coinduction tactics. To showcase the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given in an ITree-based denotational semantics. Unlike previous results using operational techniques, our bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.
@article{paperbot530,
title = {Interaction trees: representing recursive and impure programs in Coq},
author = {Li-yao Xia and Yannick Zakowski and Paul He and Chung-Kil Hur and Gregory Malecha and Benjamin C. Pierce and Steve Zdancewic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371119}
}