[isabelle] Tutorial on Deep Embeddings



I'm looking for a tutorial (or a good example or well explained description) of
how to go about creating a deep embedding of a language in Isabelle/HOL
particularly with reference to defining notions of subterm replacement
and rewriting.

Any pointers much appreciated.

Louise Dennis

--
Dr. Louise Dennis,
Department of Computer Science, Room 117, Ashton Building,
University of  Liverpool, Liverpool, L69 3BX,  UK.
http://www.csc.liv.ac.uk/~lad/  phone: +44 151 795 4237






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