In programming semantics, monads are used to provide a generic encapsulation of side-effects. We introduce a monad-based metalanguage that extends Moggi’s computational metalanguage with native exceptions and iteration, interpreted over monads supporting a dcpo structure. We present a Hoare calculus with abnormal postconditions for this metalanguage and prove relative completeness using weakest liberal preconditions, extending earlier work on the exception-free case.
CITATION STYLE
Rauch, C., Goncharov, S., & Schröder, L. (2017). Generic hoare logic for order-enriched effects with exceptions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10644 LNCS, pp. 208–222). Springer Verlag. https://doi.org/10.1007/978-3-319-72044-9_14
Mendeley helps you to discover research relevant for your work.