Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms

 

Title: Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
Author: Alexander Bentkamp (bentkamp /at/ gmail /dot/ com)
Submission date: 2018-10-19
Abstract: 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.
BibTeX:
@article{Lambda_Free_EPO-AFP,
  author  = {Alexander Bentkamp},
  title   = {Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2018,
  note    = {\url{http://isa-afp.org/entries/Lambda_Free_EPO.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Lambda_Free_RPOs