Coalgebraic structures in program construction

Coalgebraic structures in program construction (preprint)
L. S. Barbosa. In Haeusler, H. and Camarão, C., editors, Invited Tutorial at SBLP'02, Proc. 6th Brazilian Symposium on Programming Languages, Rio de Janeiro, June, 2002.

Abstract

Both initial algebras and final coalgebras are devices which provide abstract descriptions of a variety of phenomena in programming, in particular of data and behavioural structures, respectively. The former are specified by a set of constructors and well known in the programming practice. The latter resorts to a collection of observers and have been recently recognised as a promising framework to model and reason about dynamical, state-based systems. Both initiality and finality, as universal properties, entail definitional and proof principles, ie, a basis for the development of program calculi directly based on (actually driven by) type specifications. Moreover, such properties can be turned into programming combinators and used, not only to calculate programs, but also to program with. This tutorial provides a first introduction to coalgebraic structures, from a programming point of view, to foster further applications in the area of program construction.