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 http://arxiv.org/pdf/1012.4895v1.pdf)

To see its use in practice, you may also have a look at the IsaFoR/CeTA formalization
(http://cl-informatik.uibk.ac.at/software/ceta/)
which contains at least 18 definitions via partial function, where also a user-defined
monad is utilized. 

Cheers,
René
-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
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.