Email Gateway (Aug 18 2022 at 17:28): Email Gateway (Aug 18 2022 at 17:28):From: li yongjian <lyj238@gmail.com>
Dear Isabelle users:
I hear that reflection is an interesting aspect in
term-rewriting. Because Isabelle has close relationship with
function programming and term-rewriting, I believe, many experts
in Isabelle should be familar with reflection.
Who can point out some interesting work on reflection, especially
for a biginner which starts to learn reflection.
Thanks in advance.
Best
Email Gateway (Aug 18 2022 at 17:28):From: Sascha Boehme <boehmes@in.tum.de>
Hi,
For a hands-on experience to reflection in Isabelle, you may want to
have a look at this theory:
http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/ex/ReflectionEx.thy
A more in-depth application is, for example, described here:
Proof Synthesis and Reflection for Linear Arithmetic,
Amine Chaieb and Tobias Nipkow
http://www4.in.tum.de/~chaieb/pubs/pdf/linear.pdf
Also related is the following work:
A Compiled Implementation of Normalization by Evaluation
Klaus Aehlig, Florian Haftmann, and Tobias Nipkow
http://www4.in.tum.de/~nipkow/pubs/tphols08.html
Hope this helps,
Sascha
li yongjian wrote:
Last updated: Apr 26 2024 at 04:17 UTC