New up-to techniques for weak bisimulation

Up-to techniques have been introduced to enhance the bisimulation proof method for establishing bisimilarity results. While up-to techniques for strong bisimilarity are well understood, the irregularities that appear in the weak case make it difficult to give a unified presentation.We propose a uniform and modular theory of up-to techniques for weak bisimulation that captures most of the existing proof technology and introduces new techniques.Some proofs rely on nontrivial–and new–commutation results based on termination guarantees. All results presented in this paper have been formally proved using the Coq proof assistant.