Skip to Main content Skip to Navigation
Conference papers

Generic Hoare Logic for Order-Enriched Effects with Exceptions

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01767479
Contributor : Hal Ifip <>
Submitted on : Monday, April 16, 2018 - 11:35:18 AM
Last modification on : Monday, April 16, 2018 - 11:36:18 AM

File

433330_1_En_14_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Christoph Rauch, Sergey Goncharov, Lutz Schröder. Generic Hoare Logic for Order-Enriched Effects with Exceptions. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2016, Gregynog, United Kingdom. pp.208-222, ⟨10.1007/978-3-319-72044-9_14⟩. ⟨hal-01767479⟩

Share

Metrics

Record views

354

Files downloads

104