Re: [isabelle] Logic implementation in Isabelle/HOL using HOAS (Higher Order Abstract Syntax)
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.
It is usable enough for the proofs needed there, but it isn't at all practical as an implementation of first-order logic.
> On 25 Jun 2018, at 23:22, Alex Meyer <alex153 at outlook.lv> wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and