See (in the HOL4 distribution)
examples/lambda/* for quite a lot of lambda calculus based on a
nominal-sets approach and
examples/fsub for the POPLmark challenge
Both by Michael Norrish.
Konrad.
On Sun, Mar 22, 2015 at 3:04 PM, John Harrison <jr...@cl.cam.ac.uk> wrote:
>
> Petros writes:
>
> | 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?
>
> Sean McLaughlin made some sort of start on a nominal package for HOL
> Light, but I don't think it was ever completed. I have some of the
> existing code, which I hope Sean would not mind my sharing. I've
> copied him on this message in case he has anything to add.
>
> John.
>
>
> ------------------------------------------------------------------------------
> 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
