Open Bisimulation is Intuitionistic
17/6/2017: A paper on modal logics for processes is accepted at CONCUR 2017. The paper concerns a process equivalence called open bisimilarity which has desirable algebraic properties and is easily automated. 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 read it when you need a detail contained in the email. The surprising insight of our paper is that there is a fundamentally intuitionistic logical characterisation of open bisimulation.
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. 3; pp. 3:1-3:15. Leibniz International Proceedings in Informatics. DOI:10.4230/LIPIcs.CONCUR.2017.3
Slides will appear following CONCUR 2017.