Bisimilarity has been discovered rather independently in Concurrency Theory [Milner, Park] and Set Theory [Azcel, Barwise]. In both cases, bisimilarity gives a way to equate objects with infinite behavior: infinite processes in the former, non well-founded sets in the latter. The overall intuition is that we move from a stratified, inductive equality, to a coinductive one (instead of considering a least fixpoint, we consider a greatest fixpoint). One of the advantages of this approach is that it naturally comes with a powerful coinduction principle, which gives an effective method for proving equalities.

In Concurrency Theory, standard techniques can be used in order to refine this proof method: "up-to techniques". I will illustrate the usefulness of such techniques on a concrete example. I then will define a theory of such up-to techniques, at a rather abstract level: we can just work in an arbitrary complete lattice, eventually enriched with a monoid structure.