Fine by me, but I don't remember making any significant progress. Good luck!
On Sun, Mar 22, 2015 at 16:04 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
