Open Bisimulation is Intuitionistic
6/9/2017: A paper on modal logics for processes was awarded best paper at CONCUR 2017. The paper concerns a process equivalence called open bisimilarity which is easily automated and has desirable algebraic properties. Open bisimulation treats input values in a call-by-need fashion. For example, if you receive a notification that an e-mail has arrived, there is no need to immediately check the email; you can continue working and later read the email when you need a detail contained within. The surprising insight of our paper is that there is a fundamentally intuitionistic logical characterisation of open bisimulation (due to the call-by-need treatment of inputs inducing ``intuitionistic hereditary'').
Ki Yung Ahn, Ross Horne and Alwen Tiu. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. 28th International Conference on Concurrency Theory (CONCUR 2017). Editors: Roland Meyer and Uwe Nestmann; Article No. 7; pp. 7:1-7:17. Leibniz International Proceedings in Informatics. DOI:10.4230/LIPIcs.CONCUR.2017.7