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
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
There is an example of a nominal datatype in
HOL4/examples/unification/triangular/nominal.
On Wed, Mar 18, 2015 at 4:10 PM, Petros Papapanagiotou p...@ed.ac.uk
wrote:
Hello everyone,
Having reached the ceiling of what I can achieve by hacking variable
bindings and substitutions for embedded
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
