Institutions: abstract model theory for specification and programming
From MaRDI portal
Publication:4302820
DOI10.1145/147508.147524zbMath0799.68134OpenAlexW2010883554MaRDI QIDQ4302820
Joseph A. Goguen, Rod M. Burstall
Publication date: 13 November 1994
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/147508.147524
Theory of programming languages (68N15) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Categorical logic, topoi (03G30)
Related Items (only showing first 100 items - show all)
Foundations of logic programming in hybrid logics with user-defined sharing ⋮ Constructor-Based Institutions ⋮ Automating change of representation for proofs in discrete mathematics (extended version) ⋮ Lambda Expressions in Casl Architectural Specifications ⋮ A Proof Theoretic Interpretation of Model Theoretic Hiding ⋮ Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ An Institution for Graph Transformation ⋮ Compositional Modelling and Reasoning in an Institution for Processes and Data ⋮ Compositionality results for different types of parameterization and parameter passing in specification languages ⋮ Constructing systems as object communities ⋮ CSP-CASL -- a new integration of process algebra and algebraic specification ⋮ Quantifier-free logic for nondeterministic theories ⋮ Constructor-based observational logic ⋮ An institution of modal logics for coalgebras ⋮ Development graphs -- proof management for structured specifications ⋮ Algebraic-coalgebraic specification in CoCASL ⋮ Equational formulas and pattern operations in initial order-sorted algebras ⋮ Translating Testing Theories for Concurrent Systems ⋮ Ultraproducts and possible worlds semantics in institutions ⋮ Structure Formation in Large Theories ⋮ Automating Change of Representation for Proofs in Discrete Mathematics ⋮ Compositional term rewriting: An algebraic proof of Toyama's theorem ⋮ Functional sorts in data type specifications ⋮ Stratified institutions and elementary homomorphisms ⋮ Dynamic Logic with Binders and Its Application to the Development of Reactive Systems ⋮ Building Specifications in the Event-B Institution ⋮ What Is a Multi-modeling Language? ⋮ Generalized Theoroidal Institution Comorphisms ⋮ Heterogeneous Logical Environments for Distributed Specifications ⋮ Term-Generic Logic ⋮ Translating a Dependently-Typed Logic to First-Order Logic ⋮ Order-Sorted Parameterization and Induction ⋮ On the Specification and Verification of Model Transformations ⋮ Structures for abstract rewriting ⋮ Categorical abstract algebraic logic: prealgebraicity and protoalgebraicity ⋮ Categorical Abstract Algebraic Logic: Pseudo-Referential Matrix System Semantics ⋮ Herbrand theorems in arbitrary institutions ⋮ Specification of systems with parameterised events: An institution-independent approach ⋮ On the universality of atomic and molecular logics via protologics ⋮ Morphism axioms ⋮ Modularity of Ontologies in an Arbitrary Institution ⋮ An introduction to category-based equational logic ⋮ Introducing \(H\), an institution-based formal specification and verification language ⋮ Relations as abstract datatypes: An institution to specify relations between algebras ⋮ Hennessy-Milner properties via topological compactness ⋮ Algebraic methods in the compositional analysis of logic programs ⋮ Completeness of category-based equational deduction ⋮ Institutions for SQL database schemas and datasets ⋮ Term charters ⋮ Interpolation for predefined types ⋮ An Oxford survey of order sorted algebra ⋮ Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras ⋮ Exploring the structure of an algebra text with locales ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ Comorphisms of structured institutions ⋮ Algebraic implementation of abstract data types: a survey of concepts and new compositionality results ⋮ Indexed and fibred structures for Hoare logic ⋮ Unnamed Item ⋮ On quasi-varieties of multiple valued logic models ⋮ Formal reasoning about modules, reuse and their correctness ⋮ Piecewise initial algebra semantics ⋮ Institution-based encoding and verification of simple UML state machines in CASL/SPASS ⋮ Structure-preserving diagram operators ⋮ Pragmatic and semantic aspects of a module concept for graph transformation systems ⋮ Integrating Observational and Computational Features in the Specification of State-Based, Dynamical Systems ⋮ Model-Checking View-Based Partial Specifications ⋮ The institution-theoretic scope of logic theorems ⋮ Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally ⋮ Representing Model Theory in a Type-Theoretical Logical Framework ⋮ Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework ⋮ Algebra Transformation Systems as a Unifying Framework ⋮ Quantifier-free logic for multialgebraic theories ⋮ System Consequence ⋮ Change Management for Heterogeneous Development Graphs ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Model-Driven Engineering in the Heterogeneous Tool Set ⋮ Integrating Maude into Hets ⋮ Programming and symbolic computation in Maude ⋮ Channels: From Logic to Probability ⋮ Formal Properties of Modularisation ⋮ Model Finding for Recursive Functions in SMT ⋮ A formally verified abstract account of Gödel's incompleteness theorems ⋮ Interpolation and compactness in categories of pre-institutions ⋮ Hybrid Specification of Reactive Systems: An Institutional Approach ⋮ Types from Frames as Finite Automata ⋮ Query inseparability for \(\mathcal{ALC}\) ontologies ⋮ Abstract Beth definability in institutions ⋮ Comparing Meseguer's Rewriting Logic with the Logic CRWL ⋮ Institutionalising Many-Sorted Coalgebraic Modal Logic ⋮ Towards Behavioral Maude ⋮ Multi-term π-institutions and their equivalence ⋮ Formalization of universal algebra in Agda ⋮ Hierarchical hybrid logic ⋮ A Diagrammatic Logic for Object-Oriented Visual Modeling ⋮ Implicit Partiality of Signature Morphisms in Institution Theory ⋮ Omitting types theorem in hybrid dynamic first-order logic with rigid symbols ⋮ An Institutional Theory for #-Components ⋮ A Name Abstraction Functor for Named Sets ⋮ Categorical abstract algebraic logic: truth-equational \(\pi\)-institutions ⋮ Refinement in hybridised institutions
Uses Software
This page was built for publication: Institutions: abstract model theory for specification and programming
