The paper introduces the concept of "institutions" to formalize the notion of "logical system" in computing science, addressing the proliferation of various logical systems used in theorem proving and specification. Institutions are defined as categories of signatures, sentences, models, and a satisfaction relation that is consistent under changes in notation. The main results include: 1. **Gluing Theories**: Any institution where signatures can be glued together also allows gluing together theories, forming larger specifications. 2. **Constraint Handling**: Institutions can extend to include data constraints and hierarchy constraints, useful for defining abstract data types. 3. **Institution Morphisms**: Institution morphisms preserve structuring operations on theories, allowing theorem provers for one institution to be used on theories from another. 4. **Duplex and Multiplex Institutions**: These allow combining sentences and constraints from multiple institutions, with colimits inherited from the base institution. The paper also discusses the application of institutions to programming languages, database theory, and natural language semantics, emphasizing their utility in modular specification and programming. The authors provide definitions, examples, and proofs to support these concepts, including the use of category theory to formalize the notion of institutions.The paper introduces the concept of "institutions" to formalize the notion of "logical system" in computing science, addressing the proliferation of various logical systems used in theorem proving and specification. Institutions are defined as categories of signatures, sentences, models, and a satisfaction relation that is consistent under changes in notation. The main results include: 1. **Gluing Theories**: Any institution where signatures can be glued together also allows gluing together theories, forming larger specifications. 2. **Constraint Handling**: Institutions can extend to include data constraints and hierarchy constraints, useful for defining abstract data types. 3. **Institution Morphisms**: Institution morphisms preserve structuring operations on theories, allowing theorem provers for one institution to be used on theories from another. 4. **Duplex and Multiplex Institutions**: These allow combining sentences and constraints from multiple institutions, with colimits inherited from the base institution. The paper also discusses the application of institutions to programming languages, database theory, and natural language semantics, emphasizing their utility in modular specification and programming. The authors provide definitions, examples, and proofs to support these concepts, including the use of category theory to formalize the notion of institutions.