Name
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1145/2699913 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
typed lambda calculus,mathematical logic,higher-order rewriting,theory,grammars and other rewriting systems,higher-order patterns,higher-order orderings | Discrete mathematics,Combinatorics,Typed lambda calculus,Simply typed lambda calculus,System F,Rewriting,Algebraic extension,Pure type system,Dependent type,Pattern matching,Mathematics | Journal |
Volume | Issue | ISSN |
16 | 2 | 1529-3785 |
Citations | PageRank | References |
1 | 0.36 | 29 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jean-Pierre Jouannaud | 1 | 1921 | 227.43 |
| Albert Rubio | 2 | 228 | 19.44 |