The proof technique of unique solutions of contractions

This extended abstract summarises work conducted with Adrien Durier and Daniel Hirschkoff (ENS Lyon), initially reported in [38]. Bisimilarity is employed to define behavioural equivalences and reason about them. Originated in concurrency theory, bisimilarity is now widely used also in other areas, as well as outside Computer Science. In this work, behavioural equivalences, hence also bisimilarity, are meant to be weak because they abstract from internal moves of terms, as opposed to the strong ones, which make no distinctions between the internal moves and the external ones (i.e., the interactions with the environment). Weak equivalences are, practically, the most relevant ones: e.g., two equal programs may produce the same result with different numbers of evaluation steps.