Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, April 16, 2018 - 11:35:18 AM
Last modification on : Monday, April 16, 2018 - 11:36:18 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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⟩



Record views


Files downloads