| Abstract: |
The presence of computational effects, such as state, store,
exceptions, input, output, non-determinism, backtracking etc.,
complicates the reasoning about programs. In particular, usually for each
effect (or each combination of these), an own logic needs to be designed.
Monads are a well-known tool from category theory that originally has
been invented for studying algebraic structures. Monads have been used
very successfully by Moggi to model computational
effects (in particular, all of those mentioned above) in an elegent
way. This has been applied both to the semantics of programming
languages and to
the encapsulation of effects in pure functional languages such as
Haskell.
Several logics for reasoning about monadic programs have been
introduced, such as evaluation logic, Hoare
logic and dynamic
logic. Some of these
logics have a semantics and proof calculus given in a completely monad
independent (and hence, effect independent) way. We give an overview
of these logics, discuss completeness of their calculi, as well as some
application of these logics to the reasoning about Haskell and Java
programs, and a coding in the theorem prover Isabelle. |
