\begin{thebibliography}{18}
\providecommand{\natexlab}[1]{#1}
\providecommand{\url}[1]{\texttt{#1}}
\expandafter\ifx\csname urlstyle\endcsname\relax
  \providecommand{\doi}[1]{doi: #1}\else
  \providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi

\bibitem[Back and von Wright(1998)]{back-vw}
Ralph-Johan Back and Joakim von Wright.
\newblock \emph{Refinement Calculus: A Systematic Introduction}.
\newblock Graduate Texts in Computer Science, Springer, 1998.
\newblock URL
  \url{http://crest.cs.abo.fi/publications/public/1998/RefinementCalculusBook.%
pdf}.

\bibitem[Barr and Wells(1983)]{bwttt}
Michael Barr and Charles Wells.
\newblock \emph{Toposes, Triples and Theories}.
\newblock Springer-Verlag, 1983.
\newblock URL \url{http://www.cwru.edu/artsci/math/wells/pub/ttt.html}.

\bibitem[Dawson(2007{\natexlab{a}})]{dawson-cmkc}
Jeremy~E Dawson.
\newblock Compound monads and the {K}leisli category.
\newblock Unpublished note, 2007{\natexlab{a}}.
\newblock URL \url{http://users.rsise.anu.edu.au/~jeremy/pubs/cmkc/}.

\bibitem[Dawson(2004)]{dawson-fgc}
Jeremy~E Dawson.
\newblock Formalising general correctness.
\newblock In \emph{Computing: The Australasian Theory Symposium}, volume ENTCS
  {91}, pages 21--42, 2004.
\newblock URL \url{http://www.elsevier.com/locate/entcs}.

\bibitem[Dawson(2007{\natexlab{b}})]{dawson-fgs}
Jeremy~E Dawson.
\newblock Formalising generalised substitutions.
\newblock In \emph{Theorem Proving in Higher-Order Logics}, page to appear,
  2007{\natexlab{b}}.
\newblock URL \url{http://users.rsise.anu.edu.au/~jeremy/pubs/fgc/fgs/}.

\bibitem[Dijkstra(1976)]{dijkstra-gcl}
Edsger~W Dijkstra.
\newblock \emph{A Discipline of Programming}.
\newblock Prentice-Hall International, 1976.

\bibitem[Dunne(2001)]{dunne-abstr-cmds}
Steve Dunne.
\newblock Abstract commands: A uniform notation for specifications and
  implementations.
\newblock In \emph{Computing: The Australasian Theory Symposium}, volume ENTCS
  {42}, pages 104--123, 2001.
\newblock URL \url{http://www.elsevier.com/locate/entcs}.

\bibitem[Dunne(2007)]{dunne-chorus}
Steve Dunne.
\newblock Chorus angelorum.
\newblock In \emph{B 2007: Formal Specification and Development in B}, volume
  LNCS 4355, pages 19--33. Springer, 2007.

\bibitem[Dunne(2002)]{dunne-gen-subs}
Steve Dunne.
\newblock A theory of generalised substitutions.
\newblock In \emph{Formal Specification and Development in Z and B, (ZB 2002)},
  volume LNCS 2272, pages 270--290. Springer, 2002.

\bibitem[Hyland et~al.(2006)Hyland, Plotkin, and Power]{hpp-sum-tensor}
Martin Hyland, Gordon~D Plotkin, and John~A Power.
\newblock Combining effects: Sum and tensor.
\newblock \emph{Theor. Comput. Sci.}, 357:\penalty0 70--99, 2006.

\bibitem[Jacobs and Gries(1985)]{JG}
Dean Jacobs and David Gries.
\newblock General correctness: A unification of partial and total correctness.
\newblock \emph{Acta Informatica}, 22:\penalty0 67--83, 1985.

\bibitem[Jones and Duponcheel(1993)]{jd-cm}
Mark~P Jones and Luc Duponcheel.
\newblock Composing monads.
\newblock Technical Report YALEU/DCS/RR-1004, Yale University, 1993.

\bibitem[Liang et~al.(1995)Liang, Hudak, and Jones]{lhj}
Sheng Liang, Paul Hudak, and Mark~P Jones.
\newblock Monad transformers and modular interpreters.
\newblock In \emph{Symposium on Principles of Programming Languages (POPL'95)},
  pages 333--343, 1995.

\bibitem[Martin et~al.(2007)Martin, Curtis, and Rewitzky]{mcr}
Clare~E Martin, Sharon~A Curtis, and Ingrid Rewitzky.
\newblock Modelling angelic and demonic nondeterminism with multirelations.
\newblock \emph{Sci. Comput. Program.}, 65:\penalty0 140--158, 2007.

\bibitem[Moggi(1989)]{moggi-monads}
Eugenio Moggi.
\newblock Computational lambda-calculus and monads.
\newblock In \emph{Symposium on Logic in Computer Science (LICS)}. IEEE, 1989.

\bibitem[Plotkin(1976)]{plotkin-powerdomain}
Gordon~D Plotkin.
\newblock A powerdomain construction.
\newblock \emph{SIAM J.~Computing}, 5:\penalty0 452--487, 1976.

\bibitem[Rewitzky(2003)]{rewitzky-03}
Ingrid Rewitzky.
\newblock Binary multirelations.
\newblock In \emph{Theory and Applications of Relational Structures as
  Knowledge Instruments 2003}, volume LNCS 2929, pages 256--271. Springer,
  2003.

\bibitem[Wadler(1992)]{Wadler-essence}
Philip Wadler.
\newblock The essence of functional programming.
\newblock In \emph{Symposium on Principles of Programming Languages (POPL'92)},
  pages 1--14, 1992.

\end{thebibliography}
