[isabelle] Fwd: Tutorial on Deep Embeddings

Dear Fellows,

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