A library for reasoning about recursive and impure programs in Agda.
Interaction Trees(ITree) are a coinductive data structure for representing recursive and impure programs. The theory is based of the paper Interaction Trees: Representing Recursive and Impure Programs in Coq. The objective of this project is to offer an alternative implementation of the data structure in Agda.
The project is currently under active development, and many of the features discussed in the paper have not yet been fully implemented.