Re: [isabelle] reflection semantics
For a hands-on experience to reflection in Isabelle, you may want to
have a look at this theory:
A more in-depth application is, for example, described here:
Proof Synthesis and Reflection for Linear Arithmetic,
Amine Chaieb and Tobias Nipkow
Also related is the following work:
A Compiled Implementation of Normalization by Evaluation
Klaus Aehlig, Florian Haftmann, and Tobias Nipkow
Hope this helps,
li yongjian wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and