Publication:3221381
From MaRDI portal
zbMath0557.68013MaRDI QIDQ3221381
Publication date: 1985
68Q60: Specification and verification (program logics, model checking, etc.)
08B05: Equational logic, Mal'tsev conditions
68-02: Research exposition (monographs, survey articles) pertaining to computer science
68P05: Data structures
18C05: Equational categories
68N01: General topics in the theory of software
08C05: Categories of algebras
Related Items
Program specification and data refinement in type theory, Unnamed Item, Unnamed Item, Unnamed Item, FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY, Datatype laws without signatures, Goals and benchmarks for automated map reasoning, Semantic constructions for the specification of objects, Reliable agent communication -- a pragmatic perspective, The control layer in open mechanized reasoning systems: Annotations and tactics, A general framework to build contextual cover set induction provers, Algebraic nets with flexible arcs, Basic notions of universal algebra for language theory and graph grammars, Behavioural theories and the proof of behavioural properties, Using induction and rewriting to verify and complete parameterized specifications, An algebraic characterization of frontier testable tree languages, Formalizing Dijkstra's predicate transformer wp in weak second-order logic, The meaning of specifications I: Domains and initial models, Observational specifications and the indistinguishability assumption, On the Modularization Theorem for logical specifications, On the correctness of modular systems, On the role of memory in object-based and object-oriented languages, Comparison of functional and predicative query paradigms, Comparing Hagino's categorical programming language and typed lambda- calculi, On weakly confluent monadic string-rewriting systems, Algebraic approach to single-pushout graph transformation, Parallel and distributed derivations in the single-pushout approach, Categorical principles, techniques and results for high-level-replacement systems in computer science, Algebraic processing of programming languages, Polymorphic rewriting conserves algebraic strong normalization, Foundations of rule-based design of modular systems, Horn clause programs with polymorphic types: Semantics and resolution, Specification styles in distributed systems design and verification, Classes of finite relations as initial abstract data types. I, Context induction: A proof principle for behavioural abstractions and algebraic implementations, An agent calculus with simple actions where the enabling and disabling are derived operators, Some fundamental algebraic tools for the semantics of computation. III: Indexed categories, Modularising the specification of a small database system in extended ML, Semantics of order-sorted specifications, Soundness and completeness of the Birkhoff equational calculus for many-sorted algebras with possibly empty carrier sets, Algebraization of quantifier logics, an introductory overview, Temporal theories as modularisation units for concurrent system specification, An order-sorted logic for knowledge representation systems, A semi-algorithm for algebraic implementation proofs, A new method for undecidability proofs of first order theories, Denotational semantics of an object-oriented programming language with explicit wrappers, An algebraic generalization of Frege structures -- binding algebras, Models for the substitution axiom of UNITY logic, Contextual rewriting as a sound and complete proof method for conditional LOG-specifications, An algebraic semantics of higher-order types with subtypes, OBSCURE, a specification language for abstract data types, Toward formal development of programs from algebraic specifications: Parameterisation revisited, The verification of modules, Behavioural approaches to algebraic specifications. A comparative study, Another look at parameterization for oder-sorted algebraic specifications, Functorial theory of parameterized specifications in a general specification framework, On pushout consistency, modularity and interpolation for logical specifications, Actors, actions, and initiative in normative system specification, Verifying a distributed list system: A case history, A completeness theorem for the expressive power of higher-order algebraic specifications, Many-sorted algebras in congruence modular varieties, Essential concepts of algebraic specification and program development, On the complexity of specification morphisms, Order-sorted algebraic specifications with higher-order functions, May I borrow your logic? (Transporting logical structures along maps), Proof systems for structured specifications with observability operators, Institutions for logic programming, TTL: A modular language for hardware/software systems design., Proof theory of higher-order equations: Conservativity, normal forms and term rewriting., Algebraic models of correctness for abstract pipelines., Sketches and computations over fields., Object-oriented hybrid systems of coalgebras plus monoid actions, Swinging types=functions+relations+transition systems, Detecting equivalence of modular specifications with categorical diagrams, Compositional SOS and beyond: A coalgebraic view of open systems, On abstract data types presented by multiequations, Observational proofs by rewriting., Amalgamation in the semantics of CASL, Infinite hypergraphs. I: Basic properties, Algebraic models of microprocessors architecture and organisation, Relating CASL with other specification languages: the institution level., Unions of non-disjoint theories and combinations of satisfiability procedures, Compiling dyadic first-order specifications into map algebra, Structured theories and institutions, The data type variety of stack algebras, Specification and verification of object-oriented programs using supertype abstraction, Unnamed Item, Algebraic model of an interactive man?Machine environment
