The computability path order for beta-eta-normal higher-order rewriting

DOI10.1007/978-3-031-99984-0_12MaRDI QIDQ6869953zbMATH OpenFDO

Authors Aart Middeldorp

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_12

zbMATH Keywords

higher-order rewritinglambda calculustermination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A formulation of the simple theory of types
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Abstract completion, formalized
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Coq formalization of the higher-order recursive path ordering
• Higher-order rewrite systems and their confluence
• scientific article; zbMATH DE number 1722711 (Why is no real title available?)
• scientific article; zbMATH DE number 996558 (Why is no real title available?)
• scientific article; zbMATH DE number 6109844 (Why is no real title available?)
• scientific article; zbMATH DE number 1405632 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Normal higher-order termination
• Polymorphic higher-order recursive path orderings
• Polynomial interpretations for higher-order rewriting
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Termination of term rewriting: Interpretation and type elimination
• The computability path ordering
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Wanda -- a higher-order termination tool (system description)

This page was built for publication: The computability path order for beta-eta-normal higher-order rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869953)