Ground confluence of order-sorted conditional specifications modulo axioms

DOI10.1016/J.JLAMP.2019.100513MaRDI QIDQ2291829zbMATH OpenOpenAlexWikidataFDO

Authors Francisco Durán, José Meseguer, Camilo Rocha

Publication date 31 January 2020

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2019.100513

zbMATH Keywords

Maudeorder-sorted specificationsground confluenceequational programsinductive joinability proof methodsrewriting modulo axioms

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Recommendations

• Proving ground confluence of equational specifications modulo axioms
• scientific article; zbMATH DE number 3990847
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• A rationale for conditional equational programming
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories

Cites work

• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 1314876 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 3289430 (Why is no real title available?)
• A Church-Rosser checker tool for conditional order-sorted equational Maude specifications
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• CSI: new evidence -- a progress report
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• Constructors, sufficient completeness, and deadlock freedom of rewrite theories
• Folding variant narrowing and optimal variant termination
• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
• MTT: The Maude Termination Tool (System Description)
• Metalevel algorithms for variant satisfiability
• Normal forms and normal theories in conditional rewriting
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Operational termination of conditional term rewriting systems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Proving Confluence of Term Rewriting Systems Automatically
• Proving ground confluence of equational specifications modulo axioms
• Proving operational termination of membership equational programs
• Semantic foundations for generalized rewrite theories
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• Specification and proof in membership equational logic
• Strict coherence of conditional rewriting modulo axioms
• Term Rewriting and Applications
• Termination Modulo Combinations of Equational Theories
• Variant-Based Satisfiability in Initial Algebras

Cited in

(10)

• scientific article; zbMATH DE number 3990847 (Why is no real title available?)
• Optimizing Maude programs via program specialization
• Proving ground confluence of equational specifications modulo axioms
• Symbolic Specialization of Rewriting Logic Theories with Presto
• scientific article; zbMATH DE number 7455704 (Why is no real title available?)
• Programming and symbolic computation in Maude
• Guest editor's foreword
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Checking Sufficient Completeness by Inductive Theorem Proving
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

Describes a project that uses

Uses Software

• MTT
• CRC 3
• CSI
• Maude
• CafeOBJ
• OBJ3

This page was built for publication: Ground confluence of order-sorted conditional specifications modulo axioms

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