Research project HOL-MDL

Monadic Computational Logics in HOL

This project is concerned with continued work on the monadic computational logics developed by Till Mossakowski and myself, and in particular with their implementation in the theorem prover Isabelle. The project is funded by the internal research council of the University of Bremen.

The project description (in form of the grant application for the project) can be found here (only in German, I'm afraid). Some background papers can be found on my publications page -- look for anything with the words "Hoare","dynamic logic", or "exceptions" in the title.