Methods for proving termination of rewriting-based programming languages by transformation

DOI10.1016/J.ENTCS.2009.07.062MaRDI QIDQ2808239zbMATH OpenOpenAlexFDO

Authors Francisco Durán, Salvador Lucas, José Meseguer

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

toolsterm rewritingterminationrewriting logicprogram analysis and verification

Mathematics Subject Classification ID

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

Recommendations

• Transformational methodology for proving termination of logic programs
• Proving operational termination of membership equational programs
• Termination of rewriting
• MTT: The Maude Termination Tool (System Description)
• scientific article; zbMATH DE number 408800

Cites work

• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 4130339 (Why is no real title available?)
• scientific article; zbMATH DE number 3911679 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 1231656 (Why is no real title available?)
• scientific article; zbMATH DE number 1332639 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Automated Termination Analysis for Logic Programs by Term Rewriting
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• Context-sensitive rewriting strategies
• ELAN from a rewriting logic point of view
• MTT: The Maude Termination Tool (System Description)
• Operational termination of conditional term rewriting systems
• Operational termination of membership equational programs: the order-sorted way
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Order-sorted termination: the unsorted way
• Proving operational termination of membership equational programs
• Semantic foundations for generalized rewrite theories
• Specification and proof in membership equational logic
• TPA: Termination Proved Automatically
• Tyrolean termination tool: techniques and features

Cited in

(13)

• Twenty years of rewriting logic
• Operational termination of membership equational programs: the order-sorted way
• Strict coherence of conditional rewriting modulo axioms
• Proving operational termination of membership equational programs
• A Transformational Approach to Prove Outermost Termination Automatically
• Using well-founded relations for proving operational termination
• Proving termination of context-sensitive rewriting by transformation
• Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• MTT: The Maude Termination Tool (System Description)
• Applications and extensions of context-sensitive rewriting
• Transformational methodology for proving termination of logic programs
• A sound strategy to compile general recursion into finite depth pattern matching

Describes a project that uses

Uses Software

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

This page was built for publication: Methods for proving termination of rewriting-based programming languages by transformation

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