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

Alexander Bentkamp 🌐

October 19, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session Lambda_Free_EPO

Depends on

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{https://isa-afp.org/entries/Lambda_Free_EPO.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: