Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations

DOI10.1016/0304-3975(92)90302-VzbMath0778.68056MaRDI QIDQ1196302

Publication date: 16 December 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

inheritance polymorphism completeness theorem exception handling initial algebra conditional equations error recovery Birkhoff variety theorem McKinsey-Malcev quasi-variety theorem meaningless expressions sort constraints

Mathematics Subject Classification ID

Applications of universal algebra in computer science (08A70) Semantics in the theory of computing (68Q55) Ordered structures (06F99)

Related Items (only showing first 100 items - show all)

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Gordon's computer: A hardware verification case study in OBJ3 ⋮ Declarative event based models of concurrency and refinement in psi-calculi ⋮ Fuzzy terms ⋮ Bisimulation and Hidden Algebra ⋮ Constructor-Based Institutions ⋮ Equational logic and categorical semantics for multi-languages ⋮ Order-sorted equational generalization algorithm revisited ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ Equational formulas and pattern operations in initial order-sorted algebras ⋮ Another look at parameterization for oder-sorted algebraic specifications ⋮ Rewriting regular inequalities ⋮ A simple abstract semantics for equational theories ⋮ Actors, actions, and initiative in normative system specification ⋮ Verifying a distributed list system: A case history ⋮ Term-Generic Logic ⋮ Order-Sorted Parameterization and Induction ⋮ Category-based modularisation for equational logic programming ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Rewriting modulo SMT and open system analysis ⋮ Automated identification of desynchronisation attacks on shared secrets ⋮ Unification in sort theories and its applications ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ Metalevel algorithms for variant satisfiability ⋮ José Meseguer: Scientist and Friend Extraordinaire ⋮ On First-Order Model-Based Reasoning ⋮ Two Decades of Maude ⋮ Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Weak Bisimulation as a Congruence in MSOS ⋮ Proving and rewriting ⋮ An introduction to category-based equational logic ⋮ Principles of proof scores in CafeOBJ ⋮ Birkhoff style calculi for hybrid logics ⋮ Order-sorted algebraic specifications with higher-order functions ⋮ Order-sorted model theory for temporal executable specifications ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ An Oxford survey of order sorted algebra ⋮ On the semantic equivalence of language syntax formalisms ⋮ Parametrization for order-sorted algebraic specification ⋮ A modular order-sorted equational generalization algorithm ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ Unnamed Item ⋮ MTT: The Maude Termination Tool (System Description) ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Dynamically-typed computations for order-sorted equational presentations ⋮ A Decision Procedure for Bisimilarity of Generalized Regular Expressions ⋮ Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas ⋮ On multi-language abstraction. Towards a static analysis of multi-language programs ⋮ Specification and proof in membership equational logic ⋮ Semantics of order-sorted specifications ⋮ Partial derivatives of regular expressions and finite automaton constructions ⋮ Rewriting extended regular expressions ⋮ R n - and G n -logics ⋮ Higher-order algebra with transfinite types ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Multimodal logic programming using equational and order-sorted logic ⋮ Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally ⋮ Trapezoid method for solving systems of linear inequalities and its implementation in insertion modeling ⋮ Proving operational termination of membership equational programs ⋮ Order-sorted unification ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Normal forms and normal theories in conditional rewriting ⋮ Cryptographic Protocol Composition via the Authentication Tests ⋮ 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 ⋮ Applications and extensions of context-sensitive rewriting ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Regular expression order-sorted unification and matching ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Generator induction in order sorted algebras ⋮ Using well-founded relations for proving operational termination ⋮ A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy ⋮ Richer types for \(Z\) ⋮ Another definition of order-sorted algebra ⋮ Use of Logical Models for Proving Operational Termination in General Logics ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ Order-sorted algebraic specifications with higher-order functions ⋮ Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms* ⋮ Order-sorted inductive types ⋮ Termination Modulo Combinations of Equational Theories ⋮ Interpreting Abstract Interpretations in Membership Equational Logic ⋮ A hidden agenda ⋮ Capturing constrained constructor patterns in matching logic ⋮ CASL: the Common Algebraic Specification Language. ⋮ Relating CASL with other specification languages: the institution level. ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Semantics of temporal classes ⋮ A hidden Herbrand theorem: Combining the object and logic paradigms ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Executable rewriting logic semantics of Orc and formal analysis of Orc programs ⋮ A causal semantics for CCS via rewriting logic ⋮ Maude: specification and programming in rewriting logic ⋮ Logical foundations of CafeOBJ ⋮ Specification of real-time and hybrid systems in rewriting logic ⋮ Constructing specification morphisms ⋮ An algebraic semantics of higher-order types with subtypes ⋮ Symbolic computation in Maude: some tapas

Uses Software

Cites Work

This page was built for publication: Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations