Title: A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic,
Abstract: Open bisimilarity is the original notion of bisimilarity to be introduced for
the pi-calculus that is a congruence. In open bisimilarity, free names in
processes are treated as variables that may be instantiated lazily; in contrast
to early and late bisimilarity where free names are constants. We build on the
established line of work, due to Milner, Parrow, and Walker, on classical modal
logics characterising early and late bisimilarity for the $\pi$-calculus. The
important insight is, to characterise open bisimilarity, we move to the setting
of intuitionistic modal logics. The intuitionistic modal logic introduced,
called OM, is such that modalities are closed under (respectful) substitutions,
inducing a property known as intuitionistic hereditary. Intuitionistic
hereditary reflects the lazy instantiation of names in open bisimilarity. The
soundness proof for open bisimilarity with respect to the modal logic is
mechanised in Abella. The constructive content of the completeness proof
provides an algorithm for generating distinguishing formulae, where such
formulae are useful as a certificate explaining why two processes are not open
bisimilar. We draw attention to the fact that open bisimilarity is not the only
notion of bisimilarity that is a congruence: for name-passing calculi there is
a classical/intuitionistic spectrum of bisimilarities.