Email Gateway (Aug 22 2022 at 18:56): Email Gateway (Aug 22 2022 at 18:56):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce today’s other AFP entry: An Algebra for Higher-Order Terms, by Lars Hupel:
"I introduce a higher-order term algebra, generalizing the notions of free variables, matching, and substitution. The need arose from the work on a verified compiler from Isabelle to CakeML. Terms can be thought of as consisting of a generic (free variables, constants, ap- plication) and a specific part. As example applications, this entry provides instantiations for de-Bruijn terms, terms with named variables, and Blanchette’s λ-free higher-order terms. Furthermore, I implement translation functions between de-Bruijn terms and named terms and prove their correctness."
Looks like this one will go far. It’s online at
https://www.isa-afp.org/entries/Higher_Order_Terms.html
Larry Paulson
Last updated: Apr 24 2024 at 20:16 UTC