Monad-Independent Dynamic Logic in HasCasl

  • Lutz Schröder
  • Till Mossakowski
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)


Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. In previous work, we have introduced a Hoare calculus for partial correctness of monadic programs. All this has been done in an entirely monad-independent way. Here, we extend this to a monad-independent dynamic logic (assuming a moderate amount of additional infrastructure for the monad). Dynamic logic is more expressive than the Hoare calculus; in particular, it allows reasoning about termination and total correctness. As the background formalism for these concepts, we use the logic of HasCasl, a higher-order language for functional specification and programming.


Program Sequence Dynamic Logic High Order Logic Total Correctness Internal Logic 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: Casl: the Common Algebraic Specification Language. Theoret. Comput. Sci. 286, 153–196 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives,
  3. 3.
    CoFI Language Design Task Group. Casl – The CoFI Algebraic Specification Language – Summary, version 1.0. Documents/CASL/Summary. In: [2] (July 1999)Google Scholar
  4. 4.
    The Haskell mailing list (2002),
  5. 5.
    Jones, S.P., Hughes, J., Augustsson, L., Barton, D., Boutel, B., Burton, W., Fasel, J., Hammond, K., Hinze, R., Hudak, P., Johnsson, T., Jones, M., Launchbury, J., Meijer, E., Peterson, J., Reid, A., Runciman, C., Wadler, P.: Haskell 98: A non-strict, purely functional language (1999),
  6. 6.
    Loeckx, J., Sieber, K.: The Foundations of Program Verification. Wiley, Chichester (1987)CrossRefzbMATHGoogle Scholar
  7. 7.
    Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  8. 8.
    Moggi, E.: Notions of computation and monads. Inform. and Comput. 93, 55–92 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Moggi, E.: A semantics for evaluation logic. Fund. Inform. 22, 117–152 (1995)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Pitts, A.: Evaluation logic. In: Higher Order Workshop. Workshops in Computing, pp. 162–189. Springer, Heidelberg (1991)Google Scholar
  11. 11.
    Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Plotkin, G., Stirling, C.: A framework for intuitionistic modal logic. In: Theoretical Aspects of Reasoning about Knowledge. Morgan Kaufmann, San Francisco (1986)Google Scholar
  13. 13.
    Pratt, V.: Semantical considerations on Floyd-Hoare logic. In: Foundations of Computer Science, pp. 109–121. IEEE, Los Alamitos (1976)Google Scholar
  14. 14.
    Regensburger, F.: HOLCF: Higher order logic of computable functions. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 293–307. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  15. 15.
    Schröder, L.: Classifying categories for partial equational logic. In: Category Theory and Computer Science. ENTCS, vol. 69 (2002)Google Scholar
  16. 16.
    Schröder, L., Mossakowski, T.: HasCasl: Towards integrated specification and development of functional programs. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 99–116. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Schröder, L., Mossakowski, T.: Monad-independent Hoare logic in HasCasl. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 261–277. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  18. 18.
    Scott, D.S.: Relating theories of the λ-calculus. In: To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms, pp. 403–450. Academic Press, London (1980)Google Scholar
  19. 19.
    Simpson, A.K.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)Google Scholar
  20. 20.
    Wadler, P.: How to declare an imperative. ACM Computing Surveys 29, 240–263 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Lutz Schröder
    • 1
  • Till Mossakowski
    • 1
  1. 1.BISS, Department of Computer ScienceUniversity of BremenGermany

Personalised recommendations