Compound monads in specification languages
| dc.contributor.author | Dawson, Jeremy | |
| dc.coverage.spatial | Freiburg Germany | |
| dc.date.accessioned | 2015-12-10T22:13:43Z | |
| dc.date.created | October 5 2007 | |
| dc.date.issued | 2007 | |
| dc.date.updated | 2015-12-09T07:59:06Z | |
| dc.description.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. | |
| dc.identifier.isbn | 9781595936776 | |
| dc.identifier.uri | http://hdl.handle.net/1885/49875 | |
| dc.publisher | Association for Computing Machinery Inc (ACM) | |
| dc.relation.ispartofseries | Programming Languages meets Program Verification (PLPV 2007) | |
| dc.source | Proceedings of the 2007 Workshop on Programming Languages meets Program Verification (PLPV-2007) | |
| dc.source.uri | http://portal.acm.org/toc.cfm?id=1292597&type=proceeding&coll=GUIDE&dl=GUIDE&idx=SERIES824∂=series&WantType=Proceedings&title=ICFP | |
| dc.subject | Keywords: Mathematical models; Semantics; Theorem proving; Angelic choice; Distributive law for monads; Generalized substitutions; Specification languages Angelic choice; Compound monads; Demonic choice; Distributive law for monads; Extended substitutions; Generalised substitutions; Specification languages | |
| dc.title | Compound monads in specification languages | |
| dc.type | Conference paper | |
| local.bibliographicCitation.lastpage | 10 | |
| local.bibliographicCitation.startpage | 3 | |
| local.contributor.affiliation | Dawson, Jeremy, College of Engineering and Computer Science, ANU | |
| local.contributor.authoruid | Dawson, Jeremy, u8413080 | |
| local.description.embargo | 2037-12-31 | |
| local.description.notes | Imported from ARIES | |
| local.description.refereed | Yes | |
| local.identifier.absfor | 080203 - Computational Logic and Formal Languages | |
| local.identifier.absfor | 080299 - Computation Theory and Mathematics not elsewhere classified | |
| local.identifier.ariespublication | u8803936xPUB193 | |
| local.identifier.doi | 10.1145/1292597.1292600 | |
| local.identifier.scopusID | 2-s2.0-38849136450 | |
| local.type.status | Published Version |
Downloads
Original bundle
1 - 5 of 5
Loading...
- Name:
- 01_Dawson_Compound_monads_in_2007.pdf
- Size:
- 392.49 KB
- Format:
- Adobe Portable Document Format
Loading...
- Name:
- 02_Dawson_Compound_monads_in_2007.pdf
- Size:
- 43.87 KB
- Format:
- Adobe Portable Document Format
Loading...
- Name:
- 03_Dawson_Compound_monads_in_2007.pdf
- Size:
- 133.75 KB
- Format:
- Adobe Portable Document Format
Loading...
- Name:
- 04_Dawson_Compound_monads_in_2007.pdf
- Size:
- 149.91 KB
- Format:
- Adobe Portable Document Format
Loading...
- Name:
- 05_Dawson_Compound_monads_in_2007.pdf
- Size:
- 389.49 KB
- Format:
- Adobe Portable Document Format