[isabelle] Logic implementation in Isabelle/HOL using HOAS (Higher Order Abstract Syntax)



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.