A Relatively Complete Generic Hoare Logic for OrderEnriched Effects
Conference contribution
(Original article)
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: 273282
ISBN: 9781479904136
ISSN: 10436871
Abstract
Monads are the basis of a wellestablished method of encapsulating sideeffects 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 domaintheoretic settings, which allow for recursive monadic programs. Here, we lay out a definition of orderenriched monad which imposes cpo structure on the monad itself rather than on base category. Starting from the observation that orderenrichment of a monad induces a weak truthvalue object, we develop a generic Hoare calculus for monadic sideeffecting programs. For this calculus, we prove relative completeness via a calculus of weakest preconditions, which we also relate to strongest post conditions. © 2013 IEEE.
FAU Authors / FAU Editors
 Goncharov, Sergey Dr.Ing. 
  Lehrstuhl für Informatik 8 (Theoretische Informatik) 

   Lehrstuhl für Informatik 8 (Theoretische Informatik) 

How to cite
APA:  Goncharov, S., & Schröder, L. (2013). A Relatively Complete Generic Hoare Logic for OrderEnriched Effects. In Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 (pp. 273282). 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 OrderEnriched 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. 273282. 