Certification Monads

Christian Sternagel 📧 and René Thiemann 📧

October 3, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry provides several monads intended for the development of stand-alone certifiers via code generation from Isabelle/HOL. More specifically, there are three flavors of error monads (the sum type, for the case where all monadic functions are total; an instance of the former, the so called check monad, yielding either success without any further information or an error message; as well as a variant of the sum type that accommodates partial functions by providing an explicit bottom element) and a parser monad built on top. All of this monads are heavily used in the IsaFoR/CeTA project which thus provides many examples of their usage.


BSD License


Session Certification_Monads