Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
summary
Introduces a coinductive tree datatype and a ctrees monad in Coq that models nondeterminism, recursion, and effects by three node kinds: external events and two distinct nondeterministic branches, and proves fixed‑point support plus a rich equational theory. Provides bisimulation and refinement lemmas, a monad morphism embedding into itrees to reuse itree infrastructure, and two case studies building operational semantics for CCS and cooperative multithreading that mechanize equivalences and show the representation is executable and provably correct.
AI-written summary · about
chapters (16)
- 0:00Intro
- 1:12Modeling Computations in a Proof Assistant
- 2:52Notion 1: The Free Monad
- 3:31Programs as Trees
- 5:13Programs as Stateful Trees
- 5:50ITree Second Notion: Capretta's Delay Monad
- 6:41Programs as Stateful Potentially Infinite Trees
- 7:48A Reusable Library, at Scale
- 9:56Nondeterministic Branching: Which Meaning?
- 11:29Let's Take the Perspective of an LTS
- 14:08Choice Trees
- 16:27Bisimulations Over CTrees
- 17:59CTrees and Interpretation
- 19:27Calculus of Communicating Systems [Milner, 1980]
- 20:08Cooperative scheduling
- 20:49A New Tool in the Interaction Trees Environment
related talks
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
32mTyped Program Analysis Without Encodings
22mA Calculus of Inductive Linear Constructions
30mCalculating Compilers for Concurrency
20mThe Functional Essence of Imperative Binary Search Trees
21mIntrinsically Correct Algorithms and Recursive Coalgebras
01h 06mVerifying a compiler through equational means
45mA categorical view of computational effects