Ralph-Johan Back and Joakim von Wright.
 Refinement Calculus: A Systematic Introduction.
 Graduate Texts in Computer Science, Springer, 1998.
 URL
  http://crest.cs.abo.fi/publications/public/1998/RefinementCalculusBook.%
pdf.

Michael Barr and Charles Wells.
 Toposes, Triples and Theories.
 Springer-Verlag, 1983.
 URL http://www.cwru.edu/artsci/math/wells/pub/ttt.html.

Jeremy E Dawson.
 Compound monads and the Kleisli category.
 Unpublished note, 2007.
 URL http://users.rsise.anu.edu.au/~jeremy/pubs/cmkc/.

Jeremy E Dawson.
 Formalising general correctness.
 In Computing: The Australasian Theory Symposium, volume ENTCS
  91, pages 21-42, 2004.
 URL http://www.elsevier.com/locate/entcs.

Jeremy E Dawson.
 Formalising generalised substitutions.
 In Theorem Proving in Higher-Order Logics, page to appear,
  2007.
 URL http://users.rsise.anu.edu.au/~jeremy/pubs/fgc/fgs/.

Edsger W Dijkstra.
 A Discipline of Programming.
 Prentice-Hall International, 1976.

Steve Dunne.
 Abstract commands: A uniform notation for specifications and
  implementations.
 In Computing: The Australasian Theory Symposium, volume ENTCS
  42, pages 104-123, 2001.
 URL http://www.elsevier.com/locate/entcs.

Steve Dunne.
 Chorus angelorum.
 In B 2007: Formal Specification and Development in B, volume
  LNCS 4355, pages 19-33. Springer, 2007.

Steve Dunne.
 A theory of generalised substitutions.
 In Formal Specification and Development in Z and B, (ZB 2002),
  volume LNCS 2272, pages 270-290. Springer, 2002.

Martin Hyland, Gordon D Plotkin, and John A Power.
 Combining effects: Sum and tensor.
 Theor. Comput. Sci., 357: 70-99, 2006.

Dean Jacobs and David Gries.
 General correctness: A unification of partial and total correctness.
 Acta Informatica, 22: 67-83, 1985.

Mark P Jones and Luc Duponcheel.
 Composing monads.
 Technical Report YALEU/DCS/RR-1004, Yale University, 1993.

Sheng Liang, Paul Hudak, and Mark P Jones.
 Monad transformers and modular interpreters.
 In Symposium on Principles of Programming Languages (POPL'95),
  pages 333-343, 1995.

Clare E Martin, Sharon A Curtis, and Ingrid Rewitzky.
 Modelling angelic and demonic nondeterminism with multirelations.
 Sci. Comput. Program., 65: 140-158, 2007.

Eugenio Moggi.
 Computational lambda-calculus and monads.
 In Symposium on Logic in Computer Science (LICS). IEEE, 1989.

Gordon D Plotkin.
 A powerdomain construction.
 SIAM J. Computing, 5: 452-487, 1976.

Ingrid Rewitzky.
 Binary multirelations.
 In Theory and Applications of Relational Structures as
  Knowledge Instruments 2003, volume LNCS 2929, pages 256-271. Springer,
  2003.

Philip Wadler.
 The essence of functional programming.
 In Symposium on Principles of Programming Languages (POPL'92),
  pages 1-14, 1992.