Generic Hoare logic for order-enriched effects with exceptions

Christoph Rauch; Sergey Goncharov; Lutz Schröder

doi:10.1007/978-3-319-72044-9_14

Generic Hoare logic for order-enriched effects with exceptions

Christoph Rauch^*
, Sergey Goncharov
, Lutz Schröder

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers
Editors	Phillip James, Markus Roggenbach
Publisher	Springer Verlag
Pages	208-222
Number of pages	15
ISBN (Print)	9783319720432
DOIs	https://doi.org/10.1007/978-3-319-72044-9_14
Publication status	Published - 2017
Event	23rd IFIP WG 1.3 International Workshop on Algebraic Development Techniques, WADT 2016 - Gregynog, United Kingdom Duration: 21 Sept 2016 → 24 Sept 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10644 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd IFIP WG 1.3 International Workshop on Algebraic Development Techniques, WADT 2016
Country/Territory	United Kingdom
City	Gregynog
Period	21/09/16 → 24/09/16

Bibliographical note

Publisher Copyright:
© IFIP International Federation for Information Processing 2017 Published by Springer International Publishing AG 2017. All Rights Reserved.

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-72044-9_14

Cite this

Rauch, C., Goncharov, S., & Schröder, L. (2017). Generic Hoare logic for order-enriched effects with exceptions. In P. James, & M. Roggenbach (Eds.), Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers (pp. 208-222). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10644 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-72044-9_14

Rauch, Christoph ; Goncharov, Sergey ; Schröder, Lutz. / Generic Hoare logic for order-enriched effects with exceptions. Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers. editor / Phillip James ; Markus Roggenbach. Springer Verlag, 2017. pp. 208-222 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{04e82f0ab1ec4945a8bd80335db8bd5c,

title = "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{\textquoteright}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.",

author = "Christoph Rauch and Sergey Goncharov and Lutz Schr{\"o}der",

note = "Publisher Copyright: {\textcopyright} IFIP International Federation for Information Processing 2017 Published by Springer International Publishing AG 2017. All Rights Reserved.; 23rd IFIP WG 1.3 International Workshop on Algebraic Development Techniques, WADT 2016 ; Conference date: 21-09-2016 Through 24-09-2016",

year = "2017",

doi = "10.1007/978-3-319-72044-9\_14",

language = "English",

isbn = "9783319720432",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "208--222",

editor = "Phillip James and Markus Roggenbach",

booktitle = "Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers",

}

Rauch, C, Goncharov, S & Schröder, L 2017, Generic Hoare logic for order-enriched effects with exceptions. in P James & M Roggenbach (eds), Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10644 LNCS, Springer Verlag, pp. 208-222, 23rd IFIP WG 1.3 International Workshop on Algebraic Development Techniques, WADT 2016, Gregynog, United Kingdom, 21/09/16. https://doi.org/10.1007/978-3-319-72044-9_14

Generic Hoare logic for order-enriched effects with exceptions. / Rauch, Christoph; Goncharov, Sergey; Schröder, Lutz.
Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers. ed. / Phillip James; Markus Roggenbach. Springer Verlag, 2017. p. 208-222 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10644 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Generic Hoare logic for order-enriched effects with exceptions

AU - Rauch, Christoph

AU - Goncharov, Sergey

AU - Schröder, Lutz

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85038211493

U2 - 10.1007/978-3-319-72044-9_14

DO - 10.1007/978-3-319-72044-9_14

M3 - Conference contribution

AN - SCOPUS:85038211493

SN - 9783319720432

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 208

EP - 222

BT - Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers

A2 - James, Phillip

A2 - Roggenbach, Markus

PB - Springer Verlag

T2 - 23rd IFIP WG 1.3 International Workshop on Algebraic Development Techniques, WADT 2016

Y2 - 21 September 2016 through 24 September 2016

ER -

Rauch C, Goncharov S, Schröder L. Generic Hoare logic for order-enriched effects with exceptions. In James P, Roggenbach M, editors, Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers. Springer Verlag. 2017. p. 208-222. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-72044-9_14

Generic Hoare logic for order-enriched effects with exceptions

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this