We shall discuss the main constituents of the coalgebraic approach to the modelling of dynamical systems and infinite data structures.

(i) A system is modelled by a map s: S -> F(S), where S is the set of the states of the system; F(-) is the system's type (formally a functor); and where the mapping s describes the (one step) behaviour of the system, typically consisting of dynamics and observations. A pair (S, s:S -> F(S) ) is called an F-coalgebra.

(ii) Homomorphisms are functions between coalgebras preserving (and reflecting) the coalgebra structure, similarly to homomorphisms of algebras, which are mappings that preserve the operations of the algebra.

(i) and (ii) together give rise to a rich theory of dynamical systems, in which: (a) the (functor) type F of a system determines a canonical notion of system equivalence (F-bisimulation); (b) the global (infinite) behaviour as well as the minimization of systems is given by a so-called final F-coalgebra; and (c) in which coinduction is a general definition and proof principle.

In this lecture, we shall discuss the above general framework and illustrate it with various concrete examples.