Ahn, Ki YungHorne, RossTiu, Alwen2023-04-112023-04-111860-5974http://hdl.handle.net/1885/288237Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order 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 substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.We are grateful to Sam Staton for providing an example that helped us discover the completeness proof. We also appreciate the comments of the anonymous reviewers. The authors receive support from MOE Tier 2 grant MOE2014-T2-2-076. The first author receives support from NRF grant 2018R1C1B5046826 funded by Korea government (MSIT). The second author receives support from Singapore NRF grant NRF2014NCR-NCR001-30.application/pdfen-AU© 2021 The authorsbisimulationmodal logicintuitionistic logic.202110.46298/LMCS-17(3:2)20212022-01-23