Please note the exceptionally non-standard room. This is due to the BCS accreditation activity.

Abstract

Guarded induction is one of the main tools for specifying infinite objects. It has been defined and investigated syntactically, in various systems, while its semantics have often been reduced to "induction without a base case". In a recent paper, I have proposed a categorical analysis, based on an abstract notion of a guarded operation on a final coalgebra.

In the present talk, I shall outline the main ideas of that analysis, and try to explain its consequences for modelling computation. A method for constructing process categories as final coalgebras for some variants of a Familiar construction on the category of categories will also be described.