Completeness of monad-based dynamic logic

Abstract. Monads are used in functional programming as a means of modeling and encapsulating computational effects at an appropriate level of abstraction. In previous work, we have introduced monad-based dy-namic logic and have used it for the specification and verification of various monadic functional-imperative algorithms over different monads. The semantics of this logic was originally defined over partial cartesian closed categories; completeness issues were explicitly left out of consid-eration. Here, we slightly simplify the logic and reformulate it in the weaker setting of a strong monad over a cartesian category with some additional infrastructure. We provide an extended proof calculus and prove its soundness and completeness. The presence of computational effects, e.g. state, store, exceptions, input, output, non-determinism, or backtracking, substantially complicates reasoning about programs. Dealing with such features has in the past typically required dedicated logics, designed specifically for a particular combination of effects. A