Email Gateway (Aug 18 2022 at 16:49): Email Gateway (Aug 18 2022 at 16:49):From: Louise Dennis <l.a.dennis@liverpool.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
Email Gateway (Aug 18 2022 at 16:49):From: Alfio Martini <alfio.martini@acm.org>
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@liverpool.ac.uk>
Date: Thu, Jan 20, 2011 at 12:28 PM
Subject: [isabelle] Tutorial on Deep Embeddings
To: isabelle-users@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
Email Gateway (Aug 18 2022 at 16:49):From: Gergely Buday <gbuday@gmail.com>
See e.g.
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols04.html
Email Gateway (Aug 18 2022 at 16:49):From: Alfio Martini <alfio.martini@acm.org>
Thanks Gergely. The abstract itself already points to what is essential.
It will be a great read.
Cheers
Last updated: Apr 19 2024 at 08:19 UTC