Membership algebra as a logical framework for equational specification
From MaRDI portal
Recommendations
- Specification and proof in membership equational logic
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- scientific article; zbMATH DE number 2086653
- Interpreting abstract interpretations in membership equational logic
Cited in
(only showing first 100 items - show all)- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- A semantic approach to interpolation
- A rewriting logic approach to operational semantics
- Operational termination of conditional term rewriting systems
- Swinging types=functions+relations+transition systems
- Dynamic connectors for concurrency
- Compositional SOS and beyond: A coalgebraic view of open systems
- Maude: specification and programming in rewriting logic
- Reflection in conditional rewriting logic
- Logical foundations of CafeOBJ
- Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
- Specification of real-time and hybrid systems in rewriting logic
- Actor theories in rewriting logic
- A formal approach to object-oriented software engineering
- Rewriting logic: Roadmap and bibliography
- Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
- Normal forms for algebras of connections.
- Relating CASL with other specification languages: the institution level.
- Functorial models for Petri nets
- Structured theories and institutions
- Principles of proof scores in CafeOBJ
- Twenty years of rewriting logic
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Declarative debugging of rewriting logic specifications
- Verifying hierarchical Ptolemy II discrete-event models using real-time maude
- Specification and proof in membership equational logic
- Capturing constrained constructor patterns in matching logic
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Symbolic computation in Maude: some tapas
- Order-sorted equational generalization algorithm revisited
- Stability of termination and sufficient-completeness under pushouts via amalgamation
- Proving operational termination of membership equational programs
- Proving semantic properties as first-order satisfiability
- Generalized rewrite theories, coherence completion, and symbolic methods
- Programming and symbolic computation in Maude
- A partial evaluation framework for order-sorted equational programs modulo axioms
- Ground confluence of order-sorted conditional specifications modulo axioms
- Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
- Executable rewriting logic semantics of Orc and formal analysis of Orc programs
- Executable structural operational semantics in Maude
- Herbrand theorems in arbitrary institutions
- Metalevel algorithms for variant satisfiability
- A modular order-sorted equational generalization algorithm
- Semantic foundations for generalized rewrite theories
- Equational formulas and pattern operations in initial order-sorted algebras
- CINNI -- a generic calculus of explicit substitutions and its application to -, - and -calculi
- Methods for proving termination of rewriting-based programming languages by transformation
- Order-Sorted Rewriting and Congruence Closure
- Use of logical models for proving operational termination in general logics
- Metalevel algorithms for variant satisfiability
- Interpreting abstract interpretations in membership equational logic
- Comparing Meseguer's rewriting logic with the logic CRWL
- Towards behavioral Maude: behavioral membership equational logic
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- The Maude LTL model checker
- Recent advances in real-time Maude
- Abstraction and completeness for real-time Maude
- Narrowing and rewriting logic: from foundations to applications
- José Meseguer: scientist and friend extraordinaire
- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
- Two Decades of Maude
- Modularity of ontologies in an arbitrary institution
- The Formal System of Dijkstra and Scholten
- Integrating Maude into Hets
- The rewriting logic semantics project: a progress report
- Simulation and verification of synchronous set relations in rewriting logic
- Probabilistic real-time rewrite theories and their expressive power
- What Is a Multi-modeling Language?
- Declarative Debugging of Rewriting Logic Specifications
- Order-Sorted Parameterization and Induction
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Rewriting modulo SMT and open system analysis
- Declarative Debugging of Membership Equational Logic Specifications
- Effectively Checking the Finite Variant Property
- MTT: The Maude Termination Tool (System Description)
- A Modular Equational Generalization Algorithm
- The rewriting logic semantics project: a progress report
- scientific article; zbMATH DE number 1231654 (Why is no real title available?)
- scientific article; zbMATH DE number 1231659 (Why is no real title available?)
- A generic framework for n-protocol compatibility checking
- State space reduction in the Maude-NRL protocol analyzer
- Variant-Based Satisfiability in Initial Algebras
- scientific article; zbMATH DE number 2086653 (Why is no real title available?)
- Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework
- Order-sorted generalization
- scientific article; zbMATH DE number 7453112 (Why is no real title available?)
- scientific article; zbMATH DE number 7455704 (Why is no real title available?)
- Order-sorted equational unification revisited
- Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions
- Rewriting logic specification of membrane systems with promoters and inhibitors
- Strategy-based proof calculus for membrane systems
- A declarative debugger for Maude functional modules
- Variant narrowing and equational unification
- Operational termination of membership equational programs: the order-sorted way
- An institution for Object-Z with inheritance and polymorphism
- Parchments for CafeOBJ logics
- Functional logic programming in Maude
- Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
This page was built for publication: Membership algebra as a logical framework for equational specification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3839051)