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
