c © A. Tarlecki This work is licensed under the Creative Commons Attribution License. Categories, Institutions, Abstract Model Theory, and Software Specification∗

Let me start with a confession: I never properly learnt category theory, I never did any really non-trivial work in category theory, deep categorical developments always escape my understanding. I am just a naive user of the basic language of category theory — and I love it. It offers a unique toolkit to formulate many aspects of the areas I know and want to develop further at an appropriate and useful level of abstraction and generality. In this presentation I show some examples where the use of category theory, via the theory of institutions, led to beautiful, general and generic results, applicable in many different contexts, and to a better understanding of some standard classical results and ideas from mathematical logic and from the theory of algebraic specifications. The theory of institutions [2] uses the language of category theory to offer a simple formalisation of the concept of a logical system, where sentences and semantic structures are abstract objects linked by a satisfaction relation, classified by (abstract) signatures. The key tool used when working with institutions is a categorical structure imposed on the collection of signatures, together with (covariant) translations of sentences and (contravariant) reducts of semantic structures induced by signature morphisms in a way that preserves satisfaction. Nearly all (if not quite all) logical systems fit such an institutional mould. An ambitious research programme is to mimic developments that classically concern, or rely on a particula