Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.
The goal of this library is to provide a generic foundation on which to build programming languages using naturally encoded denotational semantics including (but not limited to) non-termination and effects. On top of this language, there are simulation relations and reasoning principles.
Longer term, this library should also include a core modal logic for reasoning about this language.