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. 

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.