Specifications in an arbitrary institution

DOI10.1016/0890-5401(88)90008-9zbMath0654.68017OpenAlexW2132371811MaRDI 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

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Classical first-order logic (03B10) Data structures (68P05) General topics in the theory of software (68N01)

Related Items

Structured theory presentations and logic representations, Observational logic, constructor-based logic, and their duality., A Proof Theoretic Interpretation of Model Theoretic Hiding, An Institution for Graph Transformation, Compositional Modelling and Reasoning in an Institution for Processes and Data, Constructor-based observational logic, Development graphs -- proof management for structured specifications, Structured theories and institutions, Interpolation in Grothendieck institutions, Ultraproducts and possible worlds semantics in institutions, Compositional term rewriting: An algebraic proof of Toyama's theorem, Quasi-Boolean encodings and conditionals in algebraic specification, Building Specifications in the Event-B Institution, Generalized interpolation in CASL, Heterogeneous Logical Environments for Distributed Specifications, Category-based modularisation for equational logic programming, Program specification and data refinement in type theory, Herbrand theorems in arbitrary institutions, Essential concepts of algebraic specification and program development, Specifying with syntactic theory functors, An institution-independent proof of the Robinson consistency theorem, Parameterisation for abstract structured specifications, Modularity of Ontologies in an Arbitrary Institution, Unified Algebras and action semantics, Proving correctness w.r.t. specifications with hidden parts, Logic representation in LF, A scalable module system, Principles of proof scores in CafeOBJ, Relations as abstract datatypes: An institution to specify relations between algebras, May I borrow your logic? (Transporting logical structures along maps), Proof systems for structured specifications with observability operators, Institutions for SQL database schemas and datasets, The Distributed Ontology, Modeling and Specification Language – DOL, Foundations for structuring behavioural specifications, Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras, Partialising institutions, An axiomatic approach to structuring specifications, On the existence of translations of structured specifications, Comorphisms of structured institutions, Algebraic implementation of abstract data types: a survey of concepts and new compositionality results, Grothendieck inclusion systems, Unnamed Item, Some fundamental algebraic tools for the semantics of computation. III: Indexed categories, Unnamed Item, Modularising the specification of a small database system in extended ML, Formalism and method, On behavioural abstraction and behavioural satisfaction in higher-order logic, Structure-preserving diagram operators, On the correctness of modular systems, Parchments for CafeOBJ Logics, On Automation of OTS/CafeOBJ Method, Temporal theories as modularisation units for concurrent system specification, Unnamed Item, A navigational logic for reasoning about graph properties, Property-oriented semantics of structured specifications, On the algebra of structured specifications, A categorical study on the finiteness of specifications, Amalgamation in the semantics of CASL, Structural induction in institutions, Saturated models in institutions, Institutions for navigational logics for graphical structures, Toward formal development of programs from algebraic specifications: Model-theoretic foundations, Observational interpretation of Casl specifications, A semantic approach to interpolation, Semantics of multiway dataflow constraint systems, Interpolation and compactness in categories of pre-institutions, An Institution for Object-Z with Inheritance and Polymorphism, The Foundational Legacy of ASL, CASL: the Common Algebraic Specification Language., Logical systems for structured specifications., Relating CASL with other specification languages: the institution level., Implicit Partiality of Signature Morphisms in Institution Theory, Generalised graded interpolation, On institutions for modular coalgebraic specifications., Toward formal development of programs from algebraic specifications: Parameterisation revisited

Cites Work