Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Formalization of the Embedding ...

Email Gateway (Aug 22 2022 at 18:39):

From: Tobias Nipkow <nipkow@in.tum.de>
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!
smime.p7s

Last updated: Apr 25 2024 at 20:15 UTC