Email Gateway (Aug 22 2022 at 17:29): Email Gateway (Aug 22 2022 at 17:29):From: Alex Meyer <alex153@outlook.lv>
Hello!
I am reading article about implementation of Linear Logic in Coq using parametric-HOAS http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and https://github.com/brunofx86/LL (this is notable work, because not only automation is done, but the framework allows proof of metalogic theorems as well, that is why (p)HOAS seems to be so welcome). I have heard that parametric-HOAS is not advancement but only better or worse solution and that Isabelle/HOL supports pure HOAS. My question is - is there example implementation of some logic in Isabelle/HOL using HOAS? I am aware of some implementation os sequent calculus but this is not HOAS. I guess, that there may be implementation of programming langauges (because HOAS was created exactly for that) but I am seeking especially implementation of logic with some kind of sequent calculus.
Alex
Email Gateway (Aug 22 2022 at 17:29):From: Lawrence Paulson <lp15@cam.ac.uk>
Higher-order abstract syntax has meant many different things over the years. Isabelle (that would be Isabelle/Pure rather than Isabelle/HOL) supports in the sense of having lambda binding embedded in the basic syntax. But for a long time now, HOAS has implied not only a convenient representation of lambda binding but also the possibility to include higher order syntax in inductive definitions, so that you can define for example the syntax of a functional programming language within your system and reason by induction on this syntax.
HOAS has often referred to a particular implementation of this idea suffering from the issue of "exotic terms", which is mentioned in the article you cite. I haven't seen the solution given there, although it seems to be 10 years old, and have no idea how effective it may be. In Isabelle/HOL people are much more likely to adopt the nominal approach: https://nms.kcl.ac.uk/christian.urban/Nominal/
I've done a formalisation of a first-order sequent calculus using nominal Isabelle as part of my formalisation of Gödel's incompleteness theorems.
https://www.isa-afp.org/entries/Incompleteness.html
It is usable enough for the proofs needed there, but it isn't at all practical as an implementation of first-order logic.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC