A Relatively Complete Generic Hoare Logic for Order-Enriched Effects - Goncharov, Sergey; Schröder, Lutz (Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, 2013)
Monads are the basis of a well-established method of encapsulating side-effects in semantics and programming. There have been a number of proposals for monadic program logics in the setting of plain monads, while much of the recent work on monadic semantics is concerned with monads on enriched categories, in particular in domain-theoretic settings, which allow for recursive monadic programs. Here, we lay out a definition of order-enriched monad which imposes cpo structure on the monad itself rather than on base category. Starting from the observation that order-enrichment of a monad induces a weak truth-value object, we develop a generic Hoare calculus for monadic side-effecting programs. For this calculus, we prove relative completeness via a calculus of weakest preconditions, which we also relate to strongest post conditions. © 2013 IEEE.
UnivIS-Import:2015-04-16:Pub.2013.tech.IMMD.profes_1.arelat
Keywords: computational effects; Hoare logic; monads; strongest postconditions; weakest preconditions