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
which contains at least 18 definitions via partial function, where also a user-defined
monad is utilized.
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