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

Alexander Bentkamp

19 October 2018

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.
BSD License

Depends On

Topics

Related Entries

Theories

Cite

×
@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   = October,
  year    = 2018,
  note    = {\url{http://isa-afp.org/entries/Lambda_Free_EPO.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download