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 called
```

strong 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.