Abstract

There are many situations were we have to define or reason about potentially infinite and circular objects or concepts, e.g. implicitly defined functions, lazy data types (streams, exact reals, processes, etc.).

Techniques based on coinduction are particularly useful and natural for reasoning on circular objects, in that infinite and circular objects and concepts often arise in connection with a maximal fixed point construction of some kind.

Final Semantics, originated and developed by Aczel (1988) and Rutten-Turi (1993), is an elementary categorical methodology for introducing and explaining techniques based on coinduction. The final semantics approach is driven by the operational semantics of the language, and it is dual to the syntax-driven approach of initial semantics.

The talk is divided in two parts. In the first part, we present a general theory of coinduction. In particular, we discuss set-theoretic and categorical coinduction principles, and coiteration schemes for defining morphisms into final coalgebras. We introduce also a coinductive logical system à la Gentzen for establishing largest bisimulation equivalences on circular objects.

In the second part of the talk, we show that the Final Semantics paradigm is a general methodology for giving the semantics of programming languages. We give final semantics for various process algebras, higher order imperative concurrent languages, lambda-calculus, and pi-calculus. In particular, we discuss both syntactical and semantical techniques for giving coinductive descriptions of observational equivalences in lambda-calculi.