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).
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.
https://hal.inria.fr/hal-01767479 Contributor : Hal IfipConnect 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
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⟩