Proving operational termination of membership equational programs
From MaRDI portal
Publication:2271899
DOI10.1007/s10990-008-9028-2zbMath1192.68154OpenAlexW2019496318MaRDI QIDQ2271899
Salvador Lucas, Francisco Durán, José Meseguer, Xavier Urbain, Claude Marché
Publication date: 4 August 2009
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00431474/file/duran08hosc.pdf
program transformationconditional term rewritingoperational terminationmembership equational logicdeclarative rule-based languages
Related Items
Transformations of Conditional Rewrite Systems Revisited, Sentence-normalized conditional narrowing modulo in rewriting logic and Maude, Dependency pairs for proving termination properties of conditional term rewriting systems, Rewriting modulo SMT and open system analysis, Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude, Twenty years of rewriting logic, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Local confluence of conditional and generalized term rewriting systems, Formalizing Soundness and Completeness of Unravelings, Usable Rules for Context-Sensitive Rewrite Systems, On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings, Termination of just/fair computations in term rewriting, MTT: The Maude Termination Tool (System Description), Strict coherence of conditional rewriting modulo axioms, Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures, Operational Termination of Membership Equational Programs: the Order-Sorted Way, Characterizing and proving operational termination of deterministic conditional term rewriting systems, Proving operational termination of membership equational programs, Context-sensitive dependency pairs, Normal forms and normal theories in conditional rewriting, Programming and symbolic computation in Maude, Ground confluence of order-sorted conditional specifications modulo axioms, Applications and extensions of context-sensitive rewriting, Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting, Methods for Proving Termination of Rewriting-based Programming Languages by Transformation, Using well-founded relations for proving operational termination, Use of Logical Models for Proving Operational Termination in General Logics, Termination Modulo Combinations of Equational Theories, Localized Operational Termination in General Logics
Uses Software
Cites Work
- Proving termination of context-sensitive rewriting by transformation
- 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
- Maude: specification and programming in rewriting logic
- Equational rules for rewriting logic
- Hierarchical termination revisited.
- Context-sensitive rewriting strategies
- Modular termination proofs for rewriting using dependency pairs
- Specification and proof in membership equational logic
- Proving operational termination of membership equational programs
- Modular and incremental automated termination proofs
- Modular and incremental proofs of AC-termination
- Language Prototyping: An Algebraic Specification Approach
- Unravelings and ultra-properties
- Termination of context-sensitive rewriting
- Foundations of Software Science and Computation Structures
- Frontiers of Combining Systems
- Transformation techniques for context-sensitive rewrite systems
- Term Rewriting and Applications
- Verification of Erlang processes by dependency pairs
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
