Generic Hoare Logic for Order-Enriched Effects with Exceptions - Recent Trends in Algebraic Development Techniques Access content directly
Conference Papers Year : 2017

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.
Fichier principal
Vignette du fichier
433330_1_En_14_Chapter.pdf (353.48 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01767479 , version 1 (16-04-2018)

Licence

Attribution

Identifiers

Cite

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⟩
283 View
126 Download

Altmetric

Share

Gmail Facebook X LinkedIn More