by Lutz Schröder and Till Mossakowski
Abstract:
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.
Reference:
Lutz Schröder and Till Mossakowski: Monad-independent dynamic logic in HasCASL, In Journal of Logic and Computation, 14(4), pp. 571–619, 2004. Earlier version appeared in Martin Wirsing, Dirk Pattinson, and Rolf Hennicker (eds.), Recent Trends in Algebraic Development Techniques, 16th International Workshop (WADT 2002), LNCS vol. 2755, Springer, Berlin, 2003, pp. 425-441 [preprint]
Bibtex Entry:
@Article{SchroderMossakowski03b,
author = {Lutz Schr{\"o}der and Till Mossakowski},
title = {Monad-independent dynamic logic in {HasCASL}},
year = {2004},
journal = {Journal of Logic and Computation},
volume = {14},
pages = {571--619},
number = {4},
keywords = {HasCASL CASL dynamic logic monad total correctness Hoare calculus},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2755&spage=425},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/monadicpdl.pdf"> [preprint] </a>},
psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/monadicpdl.ps},
abstract = {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.
},
note = {Earlier version appeared in Martin Wirsing, Dirk Pattinson, and Rolf Hennicker (eds.), Recent Trends in Algebraic Development Techniques, 16th International Workshop (WADT 2002), LNCS vol. 2755, Springer, Berlin, 2003, pp. 425-441},
}