一句话：提出 ctrees，一个在 Coq 中统一建模非确定性、递归与不纯程序并支持双模拟/精化推理的余归纳树单子。
本文针对在 Coq 中同时处理非确定性、递归和外部/不纯效应时缺乏统一计算模型的问题，提出 ctrees。ctrees 受 itrees 启发，将计算嵌入余归纳树，节点分为外部事件以及两类非确定性分支。这种看似冗余的设计既能以 CCS 风格浅层嵌入带内部选择的指称模型，又能恢复归纳式的 LTS 操作视图。ctrees 继承丰富的双模拟与精化工具，并建立等式理论；作者还给出从 ctrees 到 itrees 的单子态射，从而复用 itree 基础设施实现非确定性效应。最后通过 CCS 和协作式多线程两个案例研究，展示其在并发语义建模中的实用性。
This paper introduces ctrees, a monad for modeling nondeterministic, recursive, and impure programs in Coq. Inspired by Xia et al.'s itrees, this novel data structure embeds computations into coinductive trees with three kind of nodes: external events, and two variants of nondeterministic branching. This apparent redundancy allows us to provide shallow embedding of denotational models with internal choice in the style of CCS, while recovering an inductive LTS view of the computation. ctrees inherit a vast collection of bisimulation and refinement tools, with respect to which we establish a rich equational theory. We connect ctrees to the itree infrastructure by showing how a monad morphism embedding the former into the latter permits to use ctrees to implement nondeterministic effects. We demonstrate the utility of ctrees by using them to model concurrency semantics in two case studies: CCS and cooperative multithreading.
@article{paperbot2086,
title = {Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq},
author = {Nicolas Chappe and Paul He and Ludovic Henrio and Yannick Zakowski and Steve Zdancewic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571254}
}