Normal Higher-Order Termination

DOI10.1145/2699913zbMath1354.68140OpenAlexW2137965931MaRDI QIDQ2946769

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 rewritingtyped lambda calculushigher-order patternshigher-order orderings

Mathematics Subject Classification ID

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

Related Items (1)

Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Higher-order rewrite systems and their confluence
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Processes, terms and cycles: steps on the road to infinity. Essays dedicated to Jan Willem Klop on the occasion of his 60th birthday
• A Monotonic Higher-Order Semantic Path Ordering
• Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
• Higher-Order Orderings for Normal Rewriting
• The Computability Path Ordering: The End of a Quest
• Polymorphic higher-order recursive path orderings
• Computability Closure: Ten Years Later
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Simulating expansions without expansions
• Termination of rewriting in the Calculus of Constructions
• The recursive path and polynomial ordering for first-order and higher-order terms
• Higher Order Dependency Pairs for Algebraic Functional Systems
• Inductive-data-type systems

This page was built for publication: Normal Higher-Order Termination