Methods for Proving Termination of Rewriting-based Programming Languages by Transformation

DOI10.1016/j.entcs.2009.07.062zbMath1337.68067OpenAlexW2011361820MaRDI QIDQ2808239

Salvador Lucas, José Meseguer, Francisco Durán

Publication date: 20 May 2016

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.07.062

zbMATH Keywords

toolsterminationterm rewritingrewriting logicprogram analysis and verification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Applications and extensions of context-sensitive rewriting ⋮ Using well-founded relations for proving operational termination

Uses Software

• CASL
• Haskell
• OBJ3
• CafeOBJ
• Maude
• Tyrolean
• AProVE
• MTT
• MU-TERM
• TPA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tyrolean termination tool: techniques and features
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Operational termination of conditional term rewriting systems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• ELAN from a rewriting logic point of view
• Context-sensitive rewriting strategies
• Specification and proof in membership equational logic
• Proving operational termination of membership equational programs
• Semantic foundations for generalized rewrite theories
• Order-sorted termination: The unsorted way
• TPA: Termination Proved Automatically
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• MTT: The Maude Termination Tool (System Description)
• Automated Termination Analysis for Logic Programs by Term Rewriting
• Operational Termination of Membership Equational Programs: the Order-Sorted Way

This page was built for publication: Methods for Proving Termination of Rewriting-based Programming Languages by Transformation