The recursive path and polynomial ordering for first-order and higher-order terms

DOI10.1093/logcom/exs027zbMath1284.68318OpenAlexW2071764772MaRDI QIDQ4914419

Cristina Borralleras, Enric Rodríguez-Carbonell, Albert Rubio, Miquel Bofill

Publication date: 19 April 2013

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exs027

zbMATH Keywords

terminationterm rewritingtyped lambda-calculusprogram correctnessterm orderings

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Normal Higher-Order Termination, A Lambda-Free Higher-Order Recursive Path Order

Uses Software

• Tyrolean
• AProVE
• MU-TERM