一句话：提出 Rocq 中的 Choice Trees monad，用于统一建模非确定、递归和不纯程序，并复用 LTS 的互模拟与精化工具。
本文提出 Choice Trees（CTrees），一个在 Rocq 中建模非确定性、递归与不纯程序的 monad。受 ITrees 启发，CTrees 将计算嵌入含外部事件、内部步骤与延迟分支三类节点的余归纳树，从而以 CCS 风格浅嵌入带非确定性选择的指称模型，同时恢复计算的归纳 LTS 视图。借助 LTS 上成熟的互模拟与精化工具，作者建立了丰富的等式理论，并通过 monad morphism 将 CTrees 嵌入 ITrees，以支持非确定性效应实现。案例研究用 CTrees 建模 CCS 与合作式多线程的并发语义。
Abstract This paper introduces Choice Trees (CTrees), a monad for modeling nondeterministic, recursive, and impure programs in Rocq . Inspired by Xia et al .’s ((2019) Proc. ACM Program. Lang. 4 (POPL)) ITrees, this novel data structure embeds computations into coinductive trees with three kinds of nodes: external events, internal steps, and delayed branching. This structure allows us to provide shallow embedding of denotational models with nondeterministic choice in the style of ccs , while recovering an inductive LTS view of the computation. CTrees leverage a vast collection of bisimulation and refinement tools well-studied on LTSs, with respect to which we establish a rich equational theory. We connect CTrees to the ITrees infrastructure by showing how a monad morphism embedding the former into the latter permits using 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{ChappeHHIZZ25,
title = {Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq},
author = {NICOLAS CHAPPE and PAUL HE and LUDOVIC HENRIO and ELEFTHERIOS IOANNIDIS and YANNICK ZAKOWSKI and STEVE ZDANCEWIC},
journal = {Journal of Functional Programming},
volume = {35},
year = {2025},
doi = {10.1017/s0956796825100105}
}