论文标题
选择树：代表COQ中的非确定性，递归和不纯净程序
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
论文作者
论文摘要
本文介绍了Choice Trees（Crees），这是一种模型，用于对Coq中的非确定性，递归和不纯程序进行建模。受Xia等人的ITREES的启发，这种新型数据结构将计算嵌入具有三种节点的共同感应树中：外部事件和两个非确定性分支的变体。这种明显的冗余使我们能够在CCS的样式上提供具有内部选择的语音模型的浅嵌入，同时恢复了计算的诱导LTS视图。 Ctrees继承了大量的分合和精炼工具，我们建立了丰富的方程理论。 我们通过显示将前者嵌入后者允许使用CTREES实施非确定性效应的单调形态如何将CTREES连接到ITREES基础设施。我们通过在两个案例研究中使用CTREES来对并发语义进行建模：CCS和合作多线程来证明它们的实用性。
This paper introduces Choice Trees (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 itrees 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.
