[isabelle] Fwd: Tutorial on Deep Embeddings



Dear Fellows,

Related to the e-mail below, I would be grateful with any (good) pointers
(papers,
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)
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





-- 
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 MHonArc.