*To*: Alex Meyer <alex153 at outlook.lv>*Subject*: Re: [isabelle] Logic implementation in Isabelle/HOL using HOAS (Higher Order Abstract Syntax)*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 26 Jun 2018 15:19:29 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <DB5PR0401MB2197813D48A53823F3E52B1C804A0@DB5PR0401MB2197.eurprd04.prod.outlook.com>*References*: <DB5PR0401MB2197813D48A53823F3E52B1C804A0@DB5PR0401MB2197.eurprd04.prod.outlook.com>

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 > On 25 Jun 2018, at 23:22, Alex Meyer <alex153 at outlook.lv> wrote: > > 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

**References**:

- Previous by Date: [isabelle] Fix-assume in Eisbach or Isabelle/ML method?
- Next by Date: Re: [isabelle] make_string
- Previous by Thread: [isabelle] Logic implementation in Isabelle/HOL using HOAS (Higher Order Abstract Syntax)
- Next by Thread: [isabelle] Fix-assume in Eisbach or Isabelle/ML method?
- Cl-isabelle-users June 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list