Choice Trees

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

Meta

• Author(s):
  • Paul He
  • Ludovic Henrio
  • Yannick Zakowski
  • Steve Zdancewic
• License: MIT License
• Compatible Coq versions: 8.15
• Additional dependencies:
  • dune
  • Extlib
  • InteractionTrees
  • Equations
  • Coinduction
  • RelationAlgebra
  • Alectryon
• 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