Specifications in an arbitrary institution

DOI10.1016/0890-5401(88)90008-9zbMath0654.68017MaRDI QIDQ1108775

Publication date: 1988

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(88)90008-9

zbMATH Keywords

theorem proving; first-order logic; institutions; specification languages; algebraic specification; free variables

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q65: Abstract data types; algebraic specification

03B10: Classical first-order logic

68P05: Data structures

68N01: General topics in the theory of software

Related Items

Program specification and data refinement in type theory, Unnamed Item, Unnamed Item, Unnamed Item, Interpolation and compactness in categories of pre-institutions, 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, An Institution for Object-Z with Inheritance and Polymorphism, The Foundational Legacy of ASL, Parchments for CafeOBJ Logics, On Automation of OTS/CafeOBJ Method, Observational interpretation of Casl specifications, Parameterisation for abstract structured specifications, A scalable module system, Foundations for structuring behavioural specifications, An axiomatic approach to structuring specifications, On the existence of translations of structured specifications, On the algebra of structured specifications, Grothendieck inclusion systems, On behavioural abstraction and behavioural satisfaction in higher-order logic, On the correctness of modular systems, Structural induction in institutions, Quasi-Boolean encodings and conditionals in algebraic specification, Generalized interpolation in CASL, An institution-independent proof of the Robinson consistency theorem, A categorical study on the finiteness of specifications, Saturated models in institutions, A semantic approach to interpolation, Some fundamental algebraic tools for the semantics of computation. III: Indexed categories, Modularising the specification of a small database system in extended ML, Temporal theories as modularisation units for concurrent system specification, Toward formal development of programs from algebraic specifications: Parameterisation revisited, Structured theory presentations and logic representations, Essential concepts of algebraic specification and program development, May I borrow your logic? (Transporting logical structures along maps), Proof systems for structured specifications with observability operators, On institutions for modular coalgebraic specifications., Amalgamation in the semantics of CASL, CASL: the Common Algebraic Specification Language., Logical systems for structured specifications., Relating CASL with other specification languages: the institution level., Observational logic, constructor-based logic, and their duality., Structured theories and institutions, Interpolation in Grothendieck institutions, Category-based modularisation for equational logic programming, Principles of proof scores in CafeOBJ, Formalism and method, Constructor-based observational logic, Development graphs -- proof management for structured specifications, Ultraproducts and possible worlds semantics in institutions, Herbrand theorems in arbitrary institutions, Comorphisms of structured institutions, A Proof Theoretic Interpretation of Model Theoretic Hiding, An Institution for Graph Transformation, Compositional Modelling and Reasoning in an Institution for Processes and Data, Heterogeneous Logical Environments for Distributed Specifications

Cites Work