@inproceedings{58e4f696f82d4c82b9af995ef54097e1,
title = "Compound monads in specification languages",
abstract = "We consider the language of {"}extended subsitutions{"} involving both angelic and demonic choice. For other related languages expressing program semantics the implicit model of computationis based on a combination of monads by a distributive law. We show how the model of computation underlying extended subsitutions is based on a monad which, while not being a compound monad, has strong similarities to a compound monad based on a distributive law. We discuss these compound monads and monad morphisms between them. We have used the theorem prover Isabelle to formal ise and machine-check our results.",
keywords = "Angelic choice, Compound monads, Demonic choice, Distributive law for monads, Extended substitutions, Generalised substitutions, Specification languages",
author = "Dawson, \{Jeremy E.\}",
year = "2007",
doi = "10.1145/1292597.1292600",
language = "English",
isbn = "9781595936776",
series = "PLPV'07: Proceedings of the 2007 Workshop on Programming Languages meets Program Verification",
pages = "3--10",
booktitle = "PLPV'07",
note = "PLPV'07: 2007 Workshop on Programming Languages meets Program Verification ; Conference date: 05-10-2007 Through 05-10-2007",
}