The carrier sets of final coalgebras have been shown (amongst others by Jan Rutten) to be a suitable domain to model infinite datatypes or the behaviour of dynamical systems. The basic means to characterise their elements (also called states here) is the coiteration schema, which is directly related to the notion of finality. We propose the lambda-coiteration schema as a generalisation. Besides capturing other known extended formats we show that it can be used to justify definitions involving composition operators of a certain type, which are related to guarded recursive specifications.

Furthermore, the lambda-coiteration schema comes together with a proof principle that can be used to establish the bisimilarity' of states, which is the canonical notion of behavioural equivalence considered in coalgebra (also calledstrong bisimilarity' in process algebra). Conventionally such results are obtained using bisimulation relations. It turns out that one can alternatively work with relations satisfying a weaker condition that we call lambda-bisimulations. This is shown to enable considerably simpler proofs.

The resulting proof technique bears some similarity with the `bisimulation proof method' by Sangiorgi (Math. Structures in Comp. Science, 1998). The relation of the presented approach to his will be discussed in the last part of the talk.