选择树：在 Coq 中表示非确定性、递归和不纯程序
摘要：选择树（ctrees）：用于建模Coq中的非确定性、递归和非纯净程序的一种单子（monad）介绍了选择树（ctrees），这是一种新的数据结构，它将计算嵌入到具有三种类型节点的共同归纳树中：外部事件和两种非确定性分支。这种表面上的冗余允许我们以ccs的风格提供具有内部选择的表达模型的浅嵌入，同时恢复计算的归纳LTS视图。C树继承了大量的双模拟和细化工具，我们在这些工具的基础上建立了一个丰富的等式理论。我们通过展示一个单子同态的方式将选择树与itrees基础设施联系起来，该同态将前者嵌入到后者中，可用于实现非确定性效果。我们通过使用它们来模拟两个案例研究中的并发语义（ccs和协作多线程）展示了选择树的实用性。
作者：Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
论文ID：2211.06863
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-11-15