| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [21 references]
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
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