Re: [isabelle] formalising abstract machines

> Where can I find documentation on this `partial_function (option)` keyword? I did not find it in the function definition paper -- I have found its definition in an ML file but that was not very helpful.

I don't know whether this is the most recent reference, but it is described in:

A. Krauss. Recursive definitions of monadic functions. In Proc. PAR ’10, volume 43
of EPTCS, pages 1–13, 2010.

(available at

To see its use in practice, you may also have a look at the IsaFoR/CeTA formalization
which contains at least 18 definitions via partial function, where also a user-defined
monad is utilized. 

René Thiemann                    mailto:rene.thiemann at
Computational Logic Group
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.