Recursive Definitions of Monadic Functions

Details Recursive Definitions of Monadic Functions Recursive Definitions of Monadic Functions

2010-12-22

arxiv.org/abs/1012.4895v1

EPTCS 43, 2010, pp. 1-13

Computer Science

Logic in Computer Science

In Proceedings PAR 2010, arXiv:1012.4555

Scientific paper

10.4204/EPTCS.43.1

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 convenient definition principle for imperative programs, which were previously hard to define. For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.

Affiliated with

Also associated with

No associations

Rating

Recursive Definitions of Monadic Functions does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Recursive Definitions of Monadic Functions, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Recursive Definitions of Monadic Functions will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-581935