On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
From MaRDI portal
Publication:1931906
DOI10.1016/j.jlap.2011.12.004zbMath1272.03139MaRDI 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
coherence; formal verification; Maude; Church-Rosser property; rewriting modulo; order-sorted conditional specifications
68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N18: Functional programming and lambda calculus
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
68Q42: Grammars and rewriting systems
Related Items
Functional Logic Programming in Maude, Strict coherence of conditional rewriting modulo axioms, Language definitions as rewrite theories, Debugging Maude programs via runtime assertion checking and trace slicing, Sentence-normalized conditional narrowing modulo in rewriting logic and Maude, Twenty years of rewriting logic, Applications and extensions of context-sensitive rewriting, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, Ground confluence of order-sorted conditional specifications modulo axioms, Equational Abstractions in Rewriting Logic and Maude, Built-in Variant Generation and Unification, and Their Applications in Maude 2.7, 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
Uses Software
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
