Bisimulation revisited,
Luis Barbosa, UM
José Nuno Oliveira, UM
Alexandra Silva, CWI

We provide evidence of the usefulness of reasoning about process behaviour coalgebraically in the allegory of binary relations. The novelty of our approach consists in establishing a synergy between a relational construct, Reynolds' «relation on functions» involved in his abstraction theorem on parametric polymorphism (traditionally employed in explaining and reasoning about parametric polymorphism), and the coalgebraic approach to bisimulation, invariants and other concepts of process behaviour.

This synergy arises from the fact that, once pointfree-transformed, formulae in one domain «look like» others in the other domain. We stress on this syntactic aspect of formal reasoning, a kind of "let-the-symbols-do-the-work" style of calculation, often neglected by too much emphasis on domain-specific, semantic concerns.