The paper introduces the concept of "institutions" to formalize the informal notion of "logical system" in computing science. It addresses the proliferation of logical systems used in computing, such as first-order logic, equational logic, Horn-clause logic, and others. Institutions provide a general framework for abstracting away from syntactic and semantic details, enabling the definition of language features for building large structures from smaller ones without commitment to any particular logical system. Institutions are useful for specification and programming languages, as well as for areas like database theory and the semantics of artificial and natural languages. The paper presents several key results. First, it shows that any institution where signatures can be glued together also allows gluing of theories. Second, it considers when theory structuring is preserved by institution morphisms. Third, it gives conditions under which it is sound to use a theorem prover for one institution on theories from another. Fourth, it shows how to extend institutions to include various kinds of constraints useful for defining abstract data types. The paper also discusses "duplex" and "multiplex" institutions, which allow combining sentences from one institution with constraints from another. These concepts provide a flexible and rich framework for program specification and logical programming, as well as many other areas of computing science. Institutions are defined in terms of categories, with a focus on the relationship between syntax and semantics. The paper also explores the use of colimits in defining the semantics of specification languages and the role of category theory in computing science. The paper concludes with a more categorical formulation of institutions, using twisted relations and functors to define institutions and their morphisms.The paper introduces the concept of "institutions" to formalize the informal notion of "logical system" in computing science. It addresses the proliferation of logical systems used in computing, such as first-order logic, equational logic, Horn-clause logic, and others. Institutions provide a general framework for abstracting away from syntactic and semantic details, enabling the definition of language features for building large structures from smaller ones without commitment to any particular logical system. Institutions are useful for specification and programming languages, as well as for areas like database theory and the semantics of artificial and natural languages. The paper presents several key results. First, it shows that any institution where signatures can be glued together also allows gluing of theories. Second, it considers when theory structuring is preserved by institution morphisms. Third, it gives conditions under which it is sound to use a theorem prover for one institution on theories from another. Fourth, it shows how to extend institutions to include various kinds of constraints useful for defining abstract data types. The paper also discusses "duplex" and "multiplex" institutions, which allow combining sentences from one institution with constraints from another. These concepts provide a flexible and rich framework for program specification and logical programming, as well as many other areas of computing science. Institutions are defined in terms of categories, with a focus on the relationship between syntax and semantics. The paper also explores the use of colimits in defining the semantics of specification languages and the role of category theory in computing science. The paper concludes with a more categorical formulation of institutions, using twisted relations and functors to define institutions and their morphisms.