scientific article

Publication date: 1985

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

theorem proving induction computability data abstraction abstract data types initial algebra programming methodology Gödel numberings rewrite rules finality initiality computable algebras semantics of programming abstract software modules many-sorted general algebra

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) General topics in the theory of software (68N01)

Related Items

Completeness and confluence of order-sorted term rewriting, Conditional rewriting logic: Deduction, models and concurrency, Bisimulation and Hidden Algebra, Partial evaluation and \(\omega\)-completeness of algebraic specifications, On the existence of free models in abstract algebraic institutions, A recursive second order initial algebra specification of primitive recursion, Behavioural approaches to algebraic specifications. A comparative study, Toward formal development of programs from algebraic specifications: Implementations revisited, Quasi-varieties in abstract algebraic institutions, An algebraic semantics approach to the effective resolution of type equations, The data type variety of stack algebras, Divergence phenomena during completion, Algebraic specifications of computable and semicomputable data types, A completeness theorem for the expressive power of higher-order algebraic specifications, The equational theory of parameterized specifications, Modular algebraic specification of some basic geometrical constructions, Full abstraction and limiting completeness in equational languages, Metalevel algorithms for variant satisfiability, Proving and rewriting, The behavior-realization adjunction and generalized homomorphic relations, On completeness of narrowing strategies, Equational completion in order-sorted algebras, Bisimulation for probabilistic transition systems: A coalgebraic approach, A functorial framework for constraint normal logic programming, Unnamed Item, Unnamed Item, Unnamed Item, Soundness and completeness of the Birkhoff equational calculus for many-sorted algebras with possibly empty carrier sets, On behavioural abstraction and behavioural satisfaction in higher-order logic, Free objects and equational deduction for partial conditional specifications, Observational specifications and the indistinguishability assumption, Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool, Conditional rewriting logic as a unified model of concurrency, Higher-order equational logic for specification, simulation and testing, Unnamed Item, Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations, Strict coherence of conditional rewriting modulo axioms, Modal logic and algebraic specifications, Final algebras, cosemicomputable algebras and degrees of unsolvability, Computable total functions on metric algebras, universal algebraic specifications and dynamical systems, Behavioral abstraction is hiding information, Operational Termination of Membership Equational Programs: the Order-Sorted Way, Proving operational termination of membership equational programs, Order-sorted unification, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, Unnamed Item, On the complexity of reasoning in Kleene algebra, A declarative framework for object-oriented programming with genetic inheritance, Finite Basis Theorems for Relatively Congruence-Distributive Quasivarieties, Generalized rewrite theories, coherence completion, and symbolic methods, On the connection between narrowing and proof by consistency, Methods for Proving Termination of Rewriting-based Programming Languages by Transformation, On behavioural abstraction and behavioural satisfaction in higher-order logic, Data types over multiple-valued logics, Bisimulation of automata, Automatic proofs by induction in theories without constructors, Order-sorted inductive types, Swinging types=functions+relations+transition systems, A hidden agenda, Towards Behavioral Maude, Detecting equivalence of modular specifications with categorical diagrams, A hidden Herbrand theorem: Combining the object and logic paradigms, Which data types have \(\omega\)-complete initial algebra specifications?, Logical foundations of CafeOBJ