Proving operational termination of membership equational programs

DOI10.1007/s10990-008-9028-2zbMath1192.68154MaRDI 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

zbMATH Keywords

program transformation; conditional term rewriting; operational termination; membership equational logic; declarative rule-based languages

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q42: Grammars and rewriting systems

68N99: Theory of software

Related Items

Characterizing and proving operational termination of deterministic conditional term rewriting systems, Termination of just/fair computations in term rewriting, Context-sensitive dependency pairs, Proving operational termination of membership equational programs, Transformations of Conditional Rewrite Systems Revisited, Usable Rules for Context-Sensitive Rewrite Systems, MTT: The Maude Termination Tool (System Description), Termination Modulo Combinations of Equational Theories

Uses Software

• CASL
• Haskell
• OBJ3
• CafeOBJ
• Maude
• Tyrolean
• AProVE
• CiME
• MU-TERM
• CARIBOO
• Tsukuba

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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