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
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
