Operational termination of membership equational programs: the order-sorted way

DOI10.1016/J.ENTCS.2009.05.021MaRDI QIDQ5179140zbMATH OpenOpenAlexFDO

Authors Salvador Lucas, José Meseguer

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

membership equational logicoperational terminationorder-sorted equational logicprogram analysisrewriting logicterm rewriting

Mathematics Subject Classification ID

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

Recommendations

• Proving operational termination of membership equational programs
• Order-sorted termination: the unsorted way
• Strong and weak operational termination of order-sorted rewrite theories
• Methods for proving termination of rewriting-based programming languages by transformation
• Termination Modulo Combinations of Equational Theories

Cites work

• Algebraic and logic programming. Third international conference, ALP '92, Volterra, Italy, September 2--4, 1992. Proceedings
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• 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
• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 3911679 (Why is no real title available?)
• scientific article; zbMATH DE number 4060701 (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 1950449 (Why is no real title available?)
• MTT: The Maude Termination Tool (System Description)
• Operational termination of conditional term rewriting systems
• 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
• Proving termination of context-sensitive rewriting with MU-TERM
• Rewriting techniques and applications. 15th international conference, RTA 2004, Aachen, Germany, June 3--5, 2004. Proceedings.
• Semantic foundations for generalized rewrite theories
• Specification and proof in membership equational logic
• Termination of term rewriting: Interpretation and type elimination

Cited in

(13)

• Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
• Twenty years of rewriting logic
• Applications and extensions of context-sensitive rewriting
• Proving operational termination of membership equational programs
• Methods for proving termination of rewriting-based programming languages by transformation
• Use of logical models for proving operational termination in general logics
• Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
• The Formal System of Dijkstra and Scholten
• Rewriting modulo SMT and open system analysis
• MTT: The Maude Termination Tool (System Description)
• Termination Modulo Combinations of Equational Theories
• Characterizing and proving operational termination of deterministic conditional term rewriting systems
• Context-sensitive dependency pairs

Describes a project that uses

Uses Software

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

This page was built for publication: Operational termination of membership equational programs: the order-sorted way

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