CONICET | Buscador de Institutos y Recursos Humanos

This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effectsusing Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We provethat any monad morphism between a computational monad and a specification monad gives rise to a Dijkstramonad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task athand. We moreover show that a large variety of specification monads can be obtained by applying monadtransformers to various base specification monads, including predicate transformers and Hoare-style prevand postconditions. For defining correct monad transformers, we propose a language inspired by Moggi?smonadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of algebraicoperations for Dijkstra monads, and start to investigate two ways of also accommodating effect handlers. Weimplement our framework in both Coq and F*, and illustrate that it supports a wide variety of verificationstyles for effects such as exceptions, nondeterminism, state, input-output, and general recursion.