Institutions: abstract model theory for specification and programming
From MaRDI portal
Publication:4302820
DOI10.1145/147508.147524zbMath0799.68134MaRDI 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
68N15: Theory of programming languages
03B70: Logic in computer science
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68Q65: Abstract data types; algebraic specification
03G30: Categorical logic, topoi
Related Items
An Oxford survey of order sorted algebra, Interpolation and compactness in categories of pre-institutions, Completeness of category-based equational deduction, Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras, Algebraic implementation of abstract data types: a survey of concepts and new compositionality results, Object oriented institutions to specify symbolic computation systems, Observational interpretation of Casl specifications, Service Specification and Matchmaking Using Description Logic, Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems, Categorical abstract algebraic logic: Gentzenπ -institutions and the deduction-detachment property, Equational axiomatizability for coalgebra, Observational specifications and the indistinguishability assumption, On the correctness of modular systems, Behavioral abstraction is hiding information, Categorical abstract algebraic logic: \((\ell,N)\)-algebraic systems, Categorical abstract algebraic logic: models of \(\pi\)-institutions, Generalized interpolation in CASL, Remarks on classifications and adjunctions, An institution-independent proof of the Robinson consistency theorem, On model checking multiple hybrid views, An institution-independent proof of the Beth definability theorem, A semantic approach to interpolation, HasCasl: integrated higher-order specification and program development, Algebraic translations, correctness and algebraic compiler construction, From static to dynamic abstract data-types: An institution transformation, A model of reasoning about knowledge, OBSCURE, a specification language for abstract data types, Structured theory presentations and logic representations, Functorial theory of parameterized specifications in a general specification framework, Essential concepts of algebraic specification and program development, May I borrow your logic? (Transporting logical structures along maps), Institutions for logic programming, A hidden agenda, An abstract formalization of correct schemas for program synthesis, A coalgebraic equational approach to specifying observational structures, Logical foundations of CafeOBJ, Amalgamation in the semantics of CASL, Categorical abstract algebraic logic: categorical algebraization of first-order logic without terms, CASL: the Common Algebraic Specification Language., Logical systems for structured specifications., Relating CASL with other specification languages: the institution level., Semantics of temporal classes, A hidden Herbrand theorem: Combining the object and logic paradigms, Observational logic, constructor-based logic, and their duality., Structured theories and institutions, Interpolation in Grothendieck institutions, Putting consistent theories together in institutions, Institutions of variable truth values: An approach in the ordered style, Category-based modularisation for equational logic programming, Formalism and method, 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, Ultraproducts and possible worlds semantics in institutions, Piecewise initial algebra semantics, Structures for abstract rewriting, Categorical abstract algebraic logic: prealgebraicity and protoalgebraicity, Integrating Observational and Computational Features in the Specification of State-Based, Dynamical Systems, Abstract Beth definability in institutions, Multi-term π-institutions and their equivalence, Unnamed Item
Uses Software
