Interaction trees: representing recursive and impure programs in Coq
Interaction trees: representing recursive and impure programs in Coq
Interaction trees (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of “free monads,” ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers , which give meaning to …