This paper, a revised version of Rutten and Turi (1993), is part of a programme aiming at formulating a mathematical theory of structural operational semantics to complement the established theory of domains and denotational semantics to form a coherent whole (Turi 1996; Turi and Plotkin 1997). The programme is based on a suitable interplay between the induction principle, which pervades modern mathematics, and a dual, non-standard ‘coinduction principle’, which underlies many of the recursive phenomena occurring in computer science.

The aim of the present survey is to show that the elementary categorical notion of a final coalgebra is a suitable foundation for such a coinduction principle. The properties of coalgebraic coinduction are studied both at an abstract categorical level and in some specific categories used in semantics, namely categories of non-well-founded sets, partial orders and metric spaces.