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

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