Re: [Hol-info] Bindings for embedded languages in HOL
Fine by me, but I don't remember making any significant progress. Good luck! On Sun, Mar 22, 2015 at 16:04 John Harrison 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
Re: [Hol-info] Bindings for embedded languages in HOL
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 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 > -- 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
Re: [Hol-info] Bindings for embedded languages in HOL
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
Re: [Hol-info] Bindings for embedded languages in HOL
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 wrote: > 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 > -- 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
[Hol-info] Bindings for embedded languages in HOL
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
