Equations, contractions, and unique solutions

One of the most studied behavioural equivalences is bisimilarity, andthe main reason for its success is the associated bisimulation proofmethod, which can be further enhanced by means of `up-to bisimulation'techniques such as `up-to context'.A different proof method is discussed, based on unique solutions ofspecial forms of inequations called contractions, and inspired byMilner's theorem on unique-solution of equations. The method is atleast as powerful as the bisimulation proof method and its `up-tocontext' enhancements. The definition of contraction can betransferred onto other behavioural equivalences, possibly contextualand non-coinductive. This enables a coinductive reasoning style onsuch equivalences, either by applying the method based onunique-solution of contractions, or by injecting appropriatecontraction preoders into the bisimulation game.The techniques are illustrated on CCS-like languages; an example withhigher-order languages is also shown.