Goncharov S, Schröder L (2013)
Publication Type: Conference contribution, Original article
Publication year: 2013
Publisher: Institute of Electrical and Electronics Engineers
Edited Volumes: Proceedings - Symposium on Logic in Computer Science
City/Town: Los Alamitos
Pages Range: 273-282
Conference Proceedings Title: Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013
Event location: New Orleans, LA
ISBN: 978-1-4799-0413-6
DOI: 10.1109/LICS.2013.33
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.
APA:
Goncharov, S., & Schröder, L. (2013). A Relatively Complete Generic Hoare Logic for Order-Enriched Effects. In Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 (pp. 273-282). New Orleans, LA: Los Alamitos: Institute of Electrical and Electronics Engineers.
MLA:
Goncharov, Sergey, and Lutz Schröder. "A Relatively Complete Generic Hoare Logic for Order-Enriched Effects." Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA Los Alamitos: Institute of Electrical and Electronics Engineers, 2013. 273-282.
BibTeX: Download