Why if-then-else in processes should be treated intuitionistically
31/3/2018: A paper on mismatch has been accepted at LICS 2018. The paper explains why mismatch (the else branch in a statement such as "if M = N then P else Q") should be treated intuitionistically when reasoning about processes compositionally. In particular, we introduce the coarsest bisimilarity congruence for processes with if-then-else branching. The logical characterisation of this congruence is also intuitionistic, treating public information intuitionistically but private information classically. We highlight that this congruence and logic have impact in the area of verifying privacy protocols, where "else" branches avoid inadvertent leaks by providing dummy data.
Ross Horne, Ki Yung Ahn, Shang-wei Lin and Alwen Tiu. Quasi-Open Bisimilarity with Mismatch is Intuitionistic. In Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18). 10 pages. DOI:10.1145/3209108.3209125
Open Bisimilarity 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 bisimilarity 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 bisimilarity (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
Causal Attack Trees
15/3/2017: A paper on causal attack trees has been published in Fundamenta Informaticae. Causal attack trees profile the sub-goals of the proponent of an attack, by refining goals disjunctively, conjunctively and sequentially. We provide the machinery for determining whether one attack specialises another attack. Specialisation preserves correlations between answers to quantitative questions concerning attacks such as the "minimum attack time".
Ross Horne, Sjouke Mauw and Alwen Tiu. Semantics for Specialising Attack Trees based on Linear Logic. Fundamenta Informaticae 153(1-2). pp. 57-86. IOS Press. DOI:10.3233/FI-2017-1531
A supporting technical report includes proofs omitted from the journal version.
Processes as Predicates
7/6/2016: The following paper on logical systems for process calculi is published in the proceedings of CONCUR 2016. The paper introduces a new logical system, directly embedding various process calculi, not limited to Robin Milner's famous π-calculus. The trick is, to capture private names, we decompose established self-dual nominal quantifiers into a De Morgan dual pair of nominal quantifiers. Following the tradition of Gabbay and Pitts, we use Cyrillic vowels И and Э, pronounced `new' and `wen' respectively, for our pair of nominal quantifiers. The logical system opens doors for reasoning about processes, particularly for soundly reasoning about processes deployed on scalable high-availability distributed systems.
Ross Horne, Alwen Tiu, Bogdan Aman and Gabriel Ciobanu. Private Names in Non-Commutative Logic. 27th International Conference on Concurrency Theory (CONCUR 2016). Editors: Josée Desharnais and Radha Jagadeesan; Article No. 31; pp. 31:1-31:16. Leibniz International Proceedings in Informatics. DOI:10.4230/LIPIcs.CONCUR.2016.31
16/12/2015: Two papers are published on session types employing techniques from proof theory:
Ross Horne. The consistency and complexity of multiplicative additive system virtual. Scientific Annals of Computer Science, 25.2(2015): 245-316. DOI:10.7561/SACS.2015.2.245
This paper presents a consistent logical system where series-parallel composition and choice coexist happily.
Gabriel Ciobanu and Ross Horne. Behavioural analysis of sessions using the calculus of structures. In Perspectives of System Informatics, 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015. Editors: Mazzara, Manuel, Voronkov, Andrei. LNCS 9609, pages 91-106, Springer (2015). DOI:10.1007/978-3-319-41579-6_8
This paper presents a semantics for finite session types based on the above logical system. The semantics logically characterises multi-party compatibility and subtyping. This work is a tight match for the practical session modelling language Scribble and matches the approach of Deniélou and Yoshida (in the 1-buffer case). In terms of foundations, our approach follows the propositions-as-processes paradigm rather than the proofs-as-processes paradigm followed by Carbone et al.. The practical advantage of our approach is that we explicitly capture sequential composition.
Web of Linked Data
Developing Research in Computer Science
The proceedings of the workshop Embracing Global Computing in Emerging Economies (EGC2015) represents my effort to galvanise grass roots computer science research in Almaty and across the region.
Almaty, the cosmopolitan hub of Central Asia, is a magical city for winter sports, the steppe in spring, the mountains in summer and fruits of autumn.
Background and Contacts
I joined the Cyber Security Lab in the School of Computer Science and Engineering at Nanyang Technological University, Singapore, in December 2015. The project, lead by Ass.Prof. Alwen Tiu, aims to advance the state of the art for symbolic analysis of security protocols. Advances will be realised in the tool SPEC.
I defended my PhD in computer science, with a thesis titled Programming Languages and Principles for Read-Write Linked Data, in 2011 under the supervision of Prof Vladimiro Sassone at University of Southampton, UK. My BA in Mathematics and Computer Science, with first class honours and a thesis titled Computable Cyclic Functions, was awarded by Oxford University, UK, in 2005.
I collaborate mainly with Ass.Prof. Alwen Tiu, Prof. Gabriel Ciobanu and Prof. Vladimiro Sassone. I have also had the honour of collaborating with Prof Mariangiola Dezani-Ciancaglini, Dr Bogdan Aman, Dr Nicholas Gibbins, Dr Cristian Văideanu, Prof Sjouke Mauw and Dr Ki Yung Ahn. I look forward to future collaborations.