Operational Termination of Membership Equational Programs: the Order-Sorted Way

DOI10.1016/j.entcs.2009.05.021zbMath1347.68198OpenAlexW2128101632MaRDI QIDQ5179140

José Meseguer, Salvador Lucas

Publication date: 19 March 2015

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.05.021

zbMATH Keywords

program analysisterm rewritingoperational terminationrewriting logicmembership equational logicorder-sorted equational logic

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Rewriting modulo SMT and open system analysis ⋮ Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude ⋮ The Formal System of Dijkstra and Scholten ⋮ Twenty years of rewriting logic ⋮ MTT: The Maude Termination Tool (System Description) ⋮ Characterizing and proving operational termination of deterministic conditional term rewriting systems ⋮ Context-sensitive dependency pairs ⋮ Applications and extensions of context-sensitive rewriting ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Use of Logical Models for Proving Operational Termination in General Logics ⋮ Termination Modulo Combinations of Equational Theories

Uses Software

• CASL
• OBJ3
• CafeOBJ
• Maude
• AProVE
• MTT
• MU-TERM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rewriting techniques and applications. 15th international conference, RTA 2004, Aachen, Germany, June 3--5, 2004. Proceedings.
• 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
• Termination of term rewriting: Interpretation and type elimination
• CASL user manual. Introduction to using the Common Algebraic Specification Language. With chapters by Till Mossakowski, Donald Sannella, and Andrzej Tarlecki. With CD-ROM.
• Context-sensitive rewriting strategies
• Specification and proof in membership equational logic
• Proving operational termination of membership equational programs
• Semantic foundations for generalized rewrite theories
• Algebraic and logic programming. Third international conference, ALP '92, Volterra, Italy, September 2--4, 1992. Proceedings
• Proving Termination of Context-Sensitive Rewriting with MU-TERM
• Order-sorted termination: The unsorted way
• MTT: The Maude Termination Tool (System Description)

This page was built for publication: Operational Termination of Membership Equational Programs: the Order-Sorted Way