On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories

DOI10.1016/j.jlap.2011.12.004zbMath1272.03139OpenAlexW2170798886MaRDI QIDQ1931906

José Meseguer, Francisco Durán

Publication date: 16 January 2013

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2011.12.004

zbMATH Keywords

coherenceformal verificationMaudeChurch-Rosser propertyrewriting moduloorder-sorted conditional specifications

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (21)

Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ José Meseguer: Scientist and Friend Extraordinaire ⋮ Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude ⋮ Two Decades of Maude ⋮ The Formal System of Dijkstra and Scholten ⋮ Twenty years of rewriting logic ⋮ The Maude strategy language ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Functional Logic Programming in Maude ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Equational Abstractions in Rewriting Logic and Maude ⋮ Language definitions as rewrite theories ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Applications and extensions of context-sensitive rewriting ⋮ Debugging Maude programs via runtime assertion checking and trace slicing ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ Symbolic computation in Maude: some tapas

Uses Software

• Maude
• MFE
• ChC 3
• CRC 3
• MTT
• ITP
• SCC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic simulations
• Maude's module algebra
• Equational completion in order-sorted algebras
• On ground-confluence of term rewriting systems
• Equational abstractions
• 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 completion: The many-sorted way
• Semantics of order-sorted specifications
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Completion for rewriting modulo a congruence
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Completion of rewrite systems with membership constraints. II: Constraint solving
• PARLE 94, Parallel architectures and languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994. Proceedings
• On using ground joinable equations in equational theorem proving
• Equational rules for rewriting logic
• Specification and proof in membership equational logic
• Proving operational termination of membership equational programs
• Semantic foundations for generalized rewrite theories
• Methods for Proving Termination of Rewriting-based Programming Languages by Transformation
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• MTT: The Maude Termination Tool (System Description)
• State Space Reduction of Rewrite Theories Using Invisible Transitions
• Termination Modulo Combinations of Equational Theories
• Semantic confluence tests and completion methods
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• A new solution of Dijkstra's concurrent programming problem
• A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications
• A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories
• Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
• Proving ground confluence and inductive validity in constructor based equational specifications
• Order-sorted Equational Unification Revisited
• Term Rewriting and Applications

This page was built for publication: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories