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
