scientific article
From MaRDI portal
Publication:3221381
zbMath0557.68013MaRDI QIDQ3221381
Publication date: 1985
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) Equational logic, Mal'tsev conditions (08B05) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Data structures (68P05) Equational categories (18C05) General topics in the theory of software (68N01) Categories of algebras (08C05)
Related Items
A language for configuring multi-level specifications ⋮ The verification of modules ⋮ Behavioural approaches to algebraic specifications. A comparative study ⋮ Algebraic specification of modules and their basic interconnections ⋮ Toward formal development of programs from algebraic specifications: Implementations revisited ⋮ A characterization of passing compatibility for parameterized specifications ⋮ Another look at parameterization for oder-sorted algebraic specifications ⋮ Union and actualization of module specifications: Some compatibility results ⋮ Categorical aspects of data type constructors ⋮ 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 ⋮ Equational specification of partial higher-order algebras ⋮ A completeness theorem for the expressive power of higher-order algebraic specifications ⋮ Many-sorted algebras in congruence modular varieties ⋮ Functorial semantics of first-order views ⋮ A guided tour of the mathematics of MetaSoft '88 ⋮ The equational theory of parameterized specifications ⋮ Essential concepts of algebraic specification and program development ⋮ Inheritance hierarchies: Semantics and unifications ⋮ On a conjecture of Bergstra and Tucker ⋮ Attributed graph transformation with node type inheritance ⋮ Algebraic processing of programming languages ⋮ 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 ⋮ Automated flaw detection in algebraic specifications ⋮ Strategy based semantics for mobility with time and access permissions ⋮ TTL: A modular language for hardware/software systems design. ⋮ On the weaving process of aspect-oriented product family algebra ⋮ Proof theory of higher-order equations: Conservativity, normal forms and term rewriting. ⋮ Modelling evolution of communication platforms and scenarios based on transformations of high-level nets and processes ⋮ A categorical framework for the transformation of object-oriented systems: models and data ⋮ Parametrization for order-sorted algebraic specification ⋮ Combining data type and recursive process specifications using projection algebras ⋮ Observational implementation of algebraic specifications ⋮ Algebraic specification of concurrent systems ⋮ Defining, analysing and implementing communication protocols using attribute grammars ⋮ Algebraic models of correctness for abstract pipelines. ⋮ 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 ⋮ 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 ⋮ Algebraization of quantifier logics, an introductory overview ⋮ Comparison of functional and predicative query paradigms ⋮ Temporal theories as modularisation units for concurrent system specification ⋮ An order-sorted logic for knowledge representation systems ⋮ 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 ⋮ A semi-algorithm for algebraic implementation proofs ⋮ Categorical principles, techniques and results for high-level-replacement systems in computer science ⋮ A new method for undecidability proofs of first order theories ⋮ Consistent integration of models based on views of meta models ⋮ Canonical constraints for parameterized data types ⋮ Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness ⋮ Partial pushout semantics of generics in DOL ⋮ On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP ⋮ Fully abstract models and refinements as tools to compare agents in timed coordination languages ⋮ Processes with local and global liveness requirements ⋮ Denotational semantics of an object-oriented programming language with explicit wrappers ⋮ Term-rewriting systems with rule priorities ⋮ An algebraically specified language for data directed design ⋮ Data types over multiple-valued logics ⋮ Equational type logic ⋮ An algebraic generalization of Frege structures -- binding algebras ⋮ 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 ⋮ Models for the substitution axiom of UNITY logic ⋮ Petri nets and algebraic specifications ⋮ A complete axiomatic semantics of spawning ⋮ Compositional SOS and beyond: A coalgebraic view of open systems ⋮ 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 ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS ⋮ Algebraic semantics of rewriting terms and types ⋮ Consistency and semantics of equational definitions over predefined algebras ⋮ Type removal in term rewriting ⋮ Generic induction proofs ⋮ Completeness and confluence of order-sorted term rewriting ⋮ Extended term rewriting systems ⋮ Implementing term rewriting by graph reduction: Termination of combined systems ⋮ Design strategies for rewrite rules ⋮ Equational logics (birkhoff's method revisited) ⋮ Initial algebra semantics for lambda calculi ⋮ Preservation in many-valued truth institutions ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Goals and benchmarks for automated map reasoning ⋮ Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras ⋮ 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 ⋮ FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY ⋮ Compositionality results for different types of parameterization and parameter passing in specification languages ⋮ Algebraic specification and development in geometric modeling ⋮ Applications of type theory ⋮ A theory of requirements capture and its applications ⋮ Exception handling and term labelling ⋮ Constructing systems as object communities ⋮ Constructor-based observational logic ⋮ Executable structural operational semantics in Maude ⋮ Structured theories and institutions ⋮ Equational formulas and pattern operations in initial order-sorted algebras ⋮ The data type variety of stack algebras ⋮ Abstract rewriting with concrete operators ⋮ Proofs in parameterized specifications ⋮ Compositional term rewriting: An algebraic proof of Toyama's theorem ⋮ Functional sorts in data type specifications ⋮ Proof systems for structured algebraic specifications: An overview ⋮ Complexity Results for Elementary Hornets ⋮ Compatibility problems in the development of algebraic module specifications ⋮ Order-Sorted Parameterization and Induction ⋮ A domain equation for bisimulation ⋮ The monadic second-order logic of graphs. I: Recognizable sets of finite graphs ⋮ Specification and verification of object-oriented programs using supertype abstraction ⋮ Program specification and data refinement in type theory ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Applications of Algebra and Coalgebra in Scientific Modelling ⋮ Tiling algebra for constraint-based layout editing ⋮ Algebraic model of an interactive man?Machine environment ⋮ Partial arithmetical data types of rational numbers and their equational specification ⋮ Metalevel algorithms for variant satisfiability ⋮ Unified Algebras and action semantics ⋮ Proving correctness w.r.t. specifications with hidden parts ⋮ Logic programs with equational type specifications ⋮ Higher-order order-sorted algebras ⋮ First order data types and first order logic ⋮ Canonical derivations for high-level replacement systems ⋮ Single pushout transformations of equationally defined graph structures with applications to actor systems ⋮ Parameterized reachability trees for algebraic Petri nets ⋮ Proving the correctness of behavioural implementations ⋮ Detecting isomorphisms of modular specifications with diagrams ⋮ A decade of TAPSOFT ⋮ Generated models and the ω-rule: The nondeterministic case ⋮ A model inference system for generic specification with application to code sharing ⋮ Relations as abstract datatypes: An institution to specify relations between algebras ⋮ Theory of computation over stream algebras, and its applications ⋮ Algebraic methods in the compositional analysis of logic programs ⋮ Programming from metaphorisms ⋮ Double-pushout-rewriting in \(S\)-Cartesian functor categories: rewriting theory and application to partial triple graphs ⋮ Graph expressions and graph rewritings ⋮ A Tableaux System for Deontic Action Logic ⋮ Datatype laws without signatures ⋮ Automating Algebraic Specifications of Non-freely Generated Data Types ⋮ A formal definition of hierarchical predicate transition nets ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Piecewise initial algebra semantics ⋮ Fibrations and universal view updatability ⋮ The wheel of rational numbers as an abstract data type ⋮ Pragmatic and semantic aspects of a module concept for graph transformation systems ⋮ Formal relationship between graph grammars and Petri nets ⋮ Higher-order equational logic for specification, simulation and testing ⋮ From Grammars and Automata to Algebras and Coalgebras ⋮ Unnamed Item ⋮ A Conceptual and Formal Framework for the Integration of Data Type and Process Modeling Techniques ⋮ Birkhoff's variety theorem in many sorts ⋮ Visual Design of Software Architecture and Evolution based on Graph Transformation ⋮ Abstractions of data types ⋮ Amalgamation in the semantics of CASL ⋮ An algebraic semantics of event-based architectures ⋮ Verifying an infinite systolic algorithm using third-order equational methods ⋮ Abstract implementation of algebraic specifications in a temporal logic language ⋮ Unnamed Item ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ On algebraic specifications of computable algebras with the discriminator technique ⋮ Unnamed Item ⋮ Toward formal development of programs from algebraic specifications: Model-theoretic foundations ⋮ Observational interpretation of Casl specifications ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Semantics of multiway dataflow constraint systems ⋮ Infinite hypergraphs. I: Basic properties ⋮ Towards a Standard for Modular Petri Nets: A Formalisation ⋮ Hornets: Nets within Nets Combined with Net Algebra ⋮ Algebraic models of microprocessors architecture and organisation ⋮ A unifying theorem for algebraic semantics and dynamic logics ⋮ Model Transformation and Induced Instance Migration: A Universal Framework ⋮ Unnamed Item ⋮ Order-sorted algebraic specifications with higher-order functions ⋮ Labelled port graph -- a formal structure for models and computations ⋮ An Institution for Object-Z with Inheritance and Polymorphism ⋮ Abstract Constraint Data Types ⋮ The Foundational Legacy of ASL ⋮ Rule-Based Modeling and Static Analysis of Self-adaptive Systems by Graph Transformation ⋮ Relating CASL with other specification languages: the institution level. ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Fibred amalgamation, descent data, and Van Kampen squares in topoi ⋮ On abstract data types presented by multiequations ⋮ Observational proofs by rewriting. ⋮ On the complexity of stream equality ⋮ Refinement in hybridised institutions ⋮ Compiling dyadic first-order specifications into map algebra
