Specifications in an arbitrary institution
From MaRDI portal
DOI10.1016/0890-5401(88)90008-9zbMATH Open0654.68017OpenAlexW2132371811MaRDI QIDQ1108775FDOQ1108775
Authors: Donald Sannella, Andrzej Tarlecki 
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
Recommendations
first-order logictheorem provingspecification languagesinstitutionsalgebraic specificationfree variables
General topics in the theory of software (68N01) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Classical first-order logic (03B10) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- On observational equivalence and algebraic specification
- Quasi-varieties in abstract algebraic institutions
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Title not available (Why is that?)
- On the existence of free models in abstract algebraic institutions
- Partial algebras-survey of a unifying approach towards a two-valued model theory for partial algebras
- Title not available (Why is that?)
- Title not available (Why is that?)
- Why Horn formulas matter in computer science: initial structures and generic examples
- Title not available (Why is that?)
- Structured algebraic specifications: A kernel language
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Equational partiality
- Final algebra semantics and data type extensions
- Title not available (Why is that?)
- Algebraic implementation of abstract data types
- Title not available (Why is that?)
- On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types
- Final Data Types and Their Specification
- Algebraic and operational semantics of specifications allowing exceptions and errors
- Characterizing specification languages which admit initial semantics
- Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
- CLU reference manual
- Partial abstract types
- Semantics of computation
- Title not available (Why is that?)
- Axioms for abstract model theory
- Report on the Larch shared language
- The Birkhoff variety theorem for continuous algebras
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Completeness of Proof Systems for Equational Specifications
- Formal specification of a display-oriented text editor
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (89)
- Title not available (Why is that?)
- Essential concepts of algebraic specification and program development
- Relations as abstract datatypes: An institution to specify relations between algebras
- May I borrow your logic? (Transporting logical structures along maps)
- Program specification and data refinement in type theory
- On institutions for modular coalgebraic specifications.
- A scalable module system
- Temporal theories as modularisation units for concurrent system specification
- Foundations for structuring behavioural specifications
- Herbrand theorems in arbitrary institutions
- Structural induction in institutions
- Observational logic, constructor-based logic, and their duality.
- A categorical study on the finiteness of specifications
- Compositional term rewriting: An algebraic proof of Toyama's theorem
- Interpolation and compactness in categories of pre-institutions
- Parchments for CafeOBJ logics
- Principles of proof scores in CafeOBJ
- Structured theories and institutions
- On the existence of free models in abstract algebraic institutions
- Logical systems for structured specifications.
- Category-based modularisation for equational logic programming
- Some fundamental algebraic tools for the semantics of computation. III: Indexed categories
- A proof theoretic interpretation of model theoretic hiding
- Institutions for navigational logics for graphical structures
- Generalized interpolation in CASL
- An institution-independent proof of the Robinson consistency theorem
- Unified algebras and action semantics
- Title not available (Why is that?)
- Algebraic implementation of abstract data types: a survey of concepts and new compositionality results
- Observational interpretation of Casl specifications
- CASL: the Common Algebraic Specification Language.
- A semantic approach to interpolation
- Toward formal development of programs from algebraic specifications: Parameterisation revisited
- Development graphs -- proof management for structured specifications
- Amalgamation in the semantics of CASL
- Title not available (Why is that?)
- On the existence of translations of structured specifications
- Quasi-Boolean encodings and conditionals in algebraic specification
- Interpolation in Grothendieck institutions
- Constructor-based observational logic
- The distributed ontology, modeling and specification language -- DOL
- Compositional modelling and reasoning in an institution for processes and data
- Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras
- Generic constructions for behavioral specifications
- Title not available (Why is that?)
- Parameterisation for abstract structured specifications
- Proof systems for structured specifications with observability operators
- An axiomatic approach to structuring specifications
- Modularising the specification of a small database system in extended ML
- On the algebra of structured specifications
- Toward formal development of programs from algebraic specifications: model-theoretic foundations
- Grothendieck inclusion systems
- Title not available (Why is that?)
- Saturated models in institutions
- Composition of default specifications
- Structured theory presentations and logic representations
- Relating CASL with other specification languages: the institution level.
- On behavioural abstraction and behavioural satisfaction in higher-order logic
- Comorphisms of structured institutions
- What Is a derived signature morphism?
- Implicit Partiality of Signature Morphisms in Institution Theory
- On the correctness of modular systems
- Logic representation in LF
- Generalised graded interpolation
- Equivalences among various logical frameworks of partial algebras
- SpeX: a rewriting-based formal specification environment
- Proving correctness w.r.t. specifications with hidden parts
- A navigational logic for reasoning about graph properties
- An Institution for Imperative RSL Specifications
- Modularity of ontologies in an arbitrary institution
- Structure-preserving diagram operators
- (Heterogeneous) structured specifications in logics without interpolation
- An institution for Object-Z with inheritance and polymorphism
- Property-oriented semantics of structured specifications
- Partialising institutions
- Semantics of multiway dataflow constraint systems
- Specifying with syntactic theory functors
- Title not available (Why is that?)
- Title not available (Why is that?)
- The foundational legacy of ASL
- Title not available (Why is that?)
- Institutions for SQL database schemas and datasets
- Term charters
- Building Specifications in the Event-B Institution
- An institution for graph transformation
- Ultraproducts and possible worlds semantics in institutions
- On Automation of OTS/CafeOBJ Method
- Heterogeneous Logical Environments for Distributed Specifications
- Formalism and method
This page was built for publication: Specifications in an arbitrary institution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1108775)
