Skip to Main content Skip to Navigation
Journal articles

Normal Higher-Order Termination

Abstract : We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of Church's simply typed λ-calculus, and on the other hand, any use of eta, as a reduction, as an expansion or as an equation. The user's rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.
Document type :
Journal articles
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-01239068
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Monday, December 7, 2015 - 1:32:39 PM
Last modification on : Monday, November 16, 2020 - 3:56:03 PM
Long-term archiving on: : Saturday, April 29, 2017 - 9:35:59 AM

File

acmsubmission-final.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Jean-Pierre Jouannaud, Albert Rubio. Normal Higher-Order Termination. ACM Transactions on Computational Logic, Association for Computing Machinery, 2013, ⟨10.1145/26999.13⟩. ⟨hal-01239068⟩

Share

Metrics

Record views

280

Files downloads

244