[isabelle] Fwd: Tutorial on Deep Embeddings
Related to the e-mail below, I would be grateful with any (good) pointers
books?, etc) on
the topic "shallow and deep embedding of languages in (Isabelle/)HOL".
It seems to be folklore, but not for a newbie like me.
All the best!
---------- Forwarded message ----------
From: Louise Dennis <l.a.dennis at liverpool.ac.uk>
Date: Thu, Jan 20, 2011 at 12:28 PM
Subject: [isabelle] Tutorial on Deep Embeddings
To: isabelle-users at cl.cam.ac.uk
I'm looking for a tutorial (or a good example or well explained description)
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
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and