Normal higher-order termination

DOI10.1145/2699913MaRDI QIDQ2946769zbMATH OpenOpenAlexFDO

Authors Jean-Pierre Jouannaud, Albert Rubio

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2117/79284

zbMATH Keywords

higher-order orderingshigher-order patternshigher-order rewritingtyped lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• Higher-Order Orderings for Normal Rewriting
• A termination ordering for higher order rewrite systems
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• Polymorphic higher-order recursive path orderings
• A recursive path ordering for higher-order terms in η-long β-normal form

Cites work

• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A Monotonic Higher-Order Semantic Path Ordering
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Computability Closure: Ten Years Later
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Harnessing first order termination provers using higher order dependency pairs
• Higher order dependency pairs for algebraic functional systems
• Higher-Order Orderings for Normal Rewriting
• Higher-order rewrite systems and their confluence
• scientific article; zbMATH DE number 1722711 (Why is no real title available?)
• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• scientific article; zbMATH DE number 996558 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (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?)
• Inductive-data-type systems
• Orderings for term-rewriting systems
• Polymorphic higher-order recursive path orderings
• Processes, terms and cycles: steps on the road to infinity. Essays dedicated to Jan Willem Klop on the occasion of his 60th birthday
• Simulating expansions without expansions
• Termination of rewriting in the Calculus of Constructions
• The Computability Path Ordering: The End of a Quest
• The recursive path and polynomial ordering for first-order and higher-order terms

Cited in

(16)

• Proof theory of higher-order equations: Conservativity, normal forms and term rewriting.
• scientific article; zbMATH DE number 1615229 (Why is no real title available?)
• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• Higher-Order Orderings for Normal Rewriting
• Computability Closure: Ten Years Later
• scientific article; zbMATH DE number 2043542 (Why is no real title available?)
• Size-based termination of higher-order rewriting
• A termination ordering for higher order rewrite systems
• A recursive path ordering for higher-order terms in η-long β-normal form
• Polymorphic higher-order termination
• scientific article; zbMATH DE number 7566074 (Why is no real title available?)
• Polynomial interpretations for higher-order rewriting
• Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
• Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting (invited talk)
• The computability path order for beta-eta-normal higher-order rewriting
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

This page was built for publication: Normal higher-order termination

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