Dijkstra Monads Forever

This paper extends the Dijkstra monad framework, designed to write specifcations over effectful programs using monadic effects, to handle termination sensitive specifications over interactive programs. We achieve this by introducing base specification monads for non-terminating programs with uninterpreted events. We model such programs using Interaction Trees, a coinductive model for modelling programs with algebraic effects in Coq, which we further develop by adding trace semantics to achieve our goals. We also show that this approach subsumes typical, simple proof principles. We implement the framework as an extension of the Interaction Trees Coq library.