Tobias Nipkow
2018-10-21 14:06:54 UTC
Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp
This Isabelle/HOL formalization defines the Embedding Path Order (EPO) for
higher-order terms without lambda-abstraction and proves many useful properties
about it. In contrast to the lambda-free recursive path orders, it does not
fully coincide with RPO on first-order terms, but it is compatible with
arbitrary higher-order contexts.
https://www.isa-afp.org/entries/Lambda_Free_EPO.html
Enjoy!
Alexander Bentkamp
This Isabelle/HOL formalization defines the Embedding Path Order (EPO) for
higher-order terms without lambda-abstraction and proves many useful properties
about it. In contrast to the lambda-free recursive path orders, it does not
fully coincide with RPO on first-order terms, but it is compatible with
arbitrary higher-order contexts.
https://www.isa-afp.org/entries/Lambda_Free_EPO.html
Enjoy!