Compound monads in specification languages
Jeremy E. Dawson · 2007
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.