We develop a cousin of Interaction Trees, dubbed ctrees with native support for internal non-determinism.
CTree
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
git clone https://github.com/vellvm/ctrees
cd ctrees
dune build