Conference contribution
(Original article)


A Relatively Complete Generic Hoare Logic for Order-Enriched Effects


Publication Details
Author(s): Goncharov S, Schröder L
Title edited volumes: Proceedings - Symposium on Logic in Computer Science
Publisher: Institute of Electrical and Electronics Engineers
Publishing place: Los Alamitos
Publication year: 2013
Conference Proceedings Title: Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013
Pages range: 273-282
ISBN: 978-1-4799-0413-6
ISSN: 1043-6871

Event details
Event: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013
Event location: New Orleans, LA
Start date of the event: 25/06/2013
End date of the event: 28/06/2013

Abstract

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.



How to cite
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). 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
Share link
Last updated on 2017-08-17 at 02:50
PDF downloaded successfully