There is an example of a nominal datatype in
HOL4/examples/unification/triangular/nominal.
On Wed, Mar 18, 2015 at 4:10 PM, Petros Papapanagiotou <p...@ed.ac.uk>
wrote:
> Hello everyone,
>
> Having reached the ceiling of what I can achieve by "hacking" variable
> bindings and substitutions for embedded languages in HOL Light, I am now
> looking for a better way to deal with these.
>
> I have gone through some of the results of the (now almost 10yo!)
> POPLmark challenge and subsequent papers, and I am aware of the existing
> HOAS and Nominal libraries in Coq and/or Isabelle. Has anything related
> been done in HOL Light or HOL4?
>
> I came across the HOL4/examples/lambda theories. These may be just
> enough for what I need, but any pointers to other work that I have
> missed would be valuable.
>
> Thank you.
>
> Regards,
> Petros
>
>
>
>
> --
> Petros Papapanagiotou, Ph.D.
> CISA, School of Informatics
> The University of Edinburgh
>
> Email: p...@ed.ac.uk
>
> ---
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
> ------------------------------------------------------------------------------
> Dive into the World of Parallel Programming The Go Parallel Website,
> sponsored
> by Intel and developed in partnership with Slashdot Media, is your hub for
> all
> things parallel software development, from weekly thought leadership blogs
> to
> news, videos, case studies, tutorials and more. Take a look and join the
> conversation now. http://goparallel.sourceforge.net/
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
