%0 Conference Proceedings
%T Generic Hoare Logic for Order-Enriched Effects with Exceptions
%+ Friedrich-Alexander Universität Erlangen-Nürnberg = University of Erlangen-Nuremberg (FAU)
%A Rauch, Christoph
%A Goncharov, Sergey
%A Schröder, Lutz
%Z Part 4: Regular Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 23th International Workshop on Algebraic Development Techniques (WADT)
%C Gregynog, United Kingdom
%Y Phillip James
%Y Markus Roggenbach
%I Springer International Publishing
%3 Recent Trends in Algebraic Development Techniques
%V LNCS-10644
%P 208-222
%8 2016-09-21
%D 2016
%R 10.1007/978-3-319-72044-9_14
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 1
%Z WG 1.3
%2 https://inria.hal.science/hal-01767479/document
%2 https://inria.hal.science/hal-01767479/file/433330_1_En_14_Chapter.pdf
%L hal-01767479
%U https://inria.hal.science/hal-01767479
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG1-3
%~ IFIP-WADT
%~ IFIP-LNCS-10644