Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages

DOI10.1007/11805618_23zbMath1151.68444OpenAlexW2168393711MaRDI QIDQ3527303

René Thiemann, Stephan Swiderski, Peter Schneider-Kamp, Jürgen Giesl

Publication date: 25 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11805618_23

Mathematics Subject Classification ID

Theory of programming languages (68N15) Grammars and rewriting systems (68Q42)

Related Items (22)

Automatic synthesis of logical models for order-sorted first-order theories ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Mechanizing and improving dependency pairs ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Deciding Innermost Loops ⋮ Unnamed Item ⋮ The Computability Path Ordering: The End of a Quest ⋮ A Transformational Approach to Prove Outermost Termination Automatically ⋮ Termination of narrowing via termination of rewriting ⋮ Lazy productivity via termination ⋮ From Outermost Termination to Innermost Termination ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ A compact fixpoint semantics for term rewriting systems ⋮ Termination Graphs for Java Bytecode ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Loops under Strategies ⋮ Proving Termination of Integer Term Rewriting ⋮ Local Termination ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ Degrees of Undecidability in Term Rewriting ⋮ Localized Operational Termination in General Logics ⋮ Termination of Lazy Rewriting Revisited

Uses Software

• Haskell
• AProVE

This page was built for publication: Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages