Re: [isabelle] reflection semantics



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.