TY - GEN
T1 - Compound monads in specification languages
AU - Dawson, Jeremy E.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
KW - Angelic choice
KW - Compound monads
KW - Demonic choice
KW - Distributive law for monads
KW - Extended substitutions
KW - Generalised substitutions
KW - Specification languages
UR - http://www.scopus.com/inward/record.url?scp=38849136450&partnerID=8YFLogxK
U2 - 10.1145/1292597.1292600
DO - 10.1145/1292597.1292600
M3 - Conference contribution
SN - 9781595936776
T3 - PLPV'07: Proceedings of the 2007 Workshop on Programming Languages meets Program Verification
SP - 3
EP - 10
BT - PLPV'07
T2 - PLPV'07: 2007 Workshop on Programming Languages meets Program Verification
Y2 - 5 October 2007 through 5 October 2007
ER -