Choice Trees

A cousin of Interaction Trees, dubbed ctrees, with native support for internal non-determinism.

Meta

• Author(s):
  • Nicolas Chappe
  • Paul He
  • Ludovic Henrio
  • Yannick Zakowski
  • Steve Zdancewic
• License: GPLv3
• Compatible Coq versions: 8.17
• Additional dependencies:
  • dune
  • Extlib
  • InteractionTrees
  • Equations
  • Coinduction
  • RelationAlgebra
• Coq namespace: CTree

Building instructions

Installing dependencies

Installing the opam dependencies

opam install dune
opam install coq-ext-lib
opam install coq-itree
opam install coq-relation-algebra
opam install coq-coinduction
opam install coq-equations

Obtaining the project

git clone https://github.com/vellvm/ctrees
cd ctrees

Building the project

dune build

Associated publications

• Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq.
  Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic.
  POPL'23

Universe issue

Importing simultaneously some parts of the [Interaction Tree] library and of the [RelationAlgebra] library currently triggers a universe inconsistency, as discussed notably in the following issue.

Until this problem is resolved, we hence disable universe checks in part of the library via the [Unset Universe Checking] option.