Dijkstra Monads in Monadic Computation

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8446)


The Dijkstra monad has been introduced recently for capturing weakest precondition computations within the context of program verification, supported by a theorem prover. Here we give a more general description of such Dijkstra monads in a categorical setting. We first elaborate the recently developed view on program semantics in terms of a triangle of computations, state transformers, and predicate transformers. Instantiations of this triangle for different monads \(T\) show how to define the Dijkstra monad associated with \(T\), via the logic involved. Technically, we provide a morphism of monads from the state monad transformation applied to \(T\), to the Dijkstra monad associated with \(T\). This monad map is precisely the weakest precondition map in the triangle, given in categorical terms by substitution.


Complete Lattice Effect Algebra Monoidal Category Monoid Structure Weak Precondition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



Thanks to Sam Staton, Mathys Rennela, and Bas Westerbaan for their input & feedback.


  1. 1.
    Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Logic 51(1/2), 1–77 (1991)MATHMathSciNetCrossRefGoogle Scholar
  2. 2.
    Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. In: Principles of Programming Languages, pp. 90–101. ACM Press (2009)Google Scholar
  3. 3.
    D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Math. Struct. Comput. Sci. 16(3), 429–451 (2006)MATHMathSciNetCrossRefGoogle Scholar
  4. 4.
    Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer, Berlin (1990)MATHCrossRefGoogle Scholar
  5. 5.
    Dvurečenskij, A., Pulmannová, S.: New Trends in Quantum Structures. Kluwer Academic Publishers, Dordrecht (2000)MATHCrossRefGoogle Scholar
  6. 6.
    Egger, J., Møgelberg, R.E., Simpson, A.: Linearly-used continuations in the enriched effect calculus. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 18–32. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  7. 7.
    Foulis, D.J., Bennett, M.K.: Effect algebras and unsharp quantum logics. Found. Phys. 24(10), 1331–1352 (1994)MATHMathSciNetCrossRefGoogle Scholar
  8. 8.
    Furber, R., Jacobs, B.: From Kleisli categories to commutative \(C^*\)-algebras: probabilistic Gelfand duality. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 141–157. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  9. 9.
    Heinosaari, T., Ziman, M.: The Mathematical Language of Quantum Theory. From Uncertainty to Entanglement. Cambridge University Press, Cambridge (2012)MATHGoogle Scholar
  10. 10.
    Jacobs, B.: Convexity, duality and effects. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol. 323, pp. 1–19. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  11. 11.
    Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations. Book, version 2 (2012, in preparation)Google Scholar
  12. 12.
    Jacobs, B.: New directions in categorical logic, for classical, probabilistic and quantum logic. See (2014)
  13. 13.
    Jacobs, B.: Measurable spaces and their effect logic. In: Logic in Computer Science. IEEE, Computer Science Press (2013)Google Scholar
  14. 14.
    Jacobs, B., Mandemaker, J.: Coreflections in algebraic quantum logic. Found. Phys. 42(7), 932–958 (2012)MATHMathSciNetCrossRefGoogle Scholar
  15. 15.
    Jacobs, B., Mandemaker, J.: The expectation monad in quantum foundations. In: Jacobs, B., Selinger, P., Spitters, B. (eds.) Quantum Physics and Logic (QPL) 2011. Electronic Proceedings in Theoretical Computer Science, vol. 95, pp. 143–182 (2012)Google Scholar
  16. 16.
    Johnstone, P., Vickers, S.: Preframe presentations present. In: Carboni, A., Pedicchio, M.C., Rosolini, G. (eds.) Como Conference on Category Theory. Lecture Notes in Mathematics, vol. 1488, pp. 193–212. Springer, Berlin (1991)CrossRefGoogle Scholar
  17. 17.
    Lawvere, F.: Ordinal sums and equational doctrines. In: Eckman, B. (ed.) Seminar on Triples and Categorical Homology Theory. Lecture Notes in Mathematics, vol. 80, pp. 141–155. Springer, Berlin (1969)CrossRefGoogle Scholar
  18. 18.
    Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Principles of Programming Languages, pp. 333–343. ACM Press (1995)Google Scholar
  19. 19.
    Manes, E.: A triple-theoretic construction of compact algebras. In: Eckman, B. (ed.) Seminar on Triples and Categorical Homology Theory. Lecture Notes in Mathematics, vol. 80, pp. 91–118. Springer, Berlin (1969)CrossRefGoogle Scholar
  20. 20.
    Maruyama, Y.: Categorical duality theory: with applications to domains, convexity, and the distribution monad. In: Ronchi Della Rocca, S. (ed.) Computer Science Logic. Leibniz International Proceedings in Informatics, pp. 500–520 (2013)Google Scholar
  21. 21.
    Mac Lane, S.: Categories for the Working Mathematician. Springer, Berlin (1971)MATHCrossRefGoogle Scholar
  22. 22.
    Møgelberg, R.E., Staton, S.: Linearly-used state in models of call-by-value. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 298–313. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  23. 23.
    Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)MATHMathSciNetCrossRefGoogle Scholar
  24. 24.
    Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: International Conference on Functional Programming (ICFP). ACM SIGPLAN Notices, pp. 229–240 (2008)Google Scholar
  25. 25.
    Plotkin, G., Power, J.: Computational effects and operations: an overview. In: Proceedings of the Workshop on Domains VI. Electronic Notes in Theoretical Computer Science, vol. 73, pp. 149–163. Elsevier, Amsterdam (2004)Google Scholar
  26. 26.
    Pulmannová, S., Gudder, S.: Representation theorem for convex effect algebras. Commentat. Math. Univ. Carol. 39(4), 645–659 (1998)MATHGoogle Scholar
  27. 27.
    Stone, M.: Postulates for the barycentric calculus. Ann. Math. 29, 25–30 (1949)MATHGoogle Scholar
  28. 28.
    Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 387–398. ACM (2013)Google Scholar
  29. 29.
    Swierstra, W.: A Hoare logic for the state monad. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 440–451. Springer, Heidelberg (2009) CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2014

Authors and Affiliations

  1. 1.Institute for Computing and Information Sciences (iCIS)Radboud University NijmegenNijmegenThe Netherlands

Personalised recommendations