Recursive Definitions of Monadic Functions

Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a conve...

Full description

Bibliographic Details
Main Author: Alexander Krauss
Format: Article
Language:English
Published: Open Publishing Association 2010-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1012.4895v1