[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
Any pointers much appreciated.
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