Research Fellow

Dr Ross Horne

News on Selected Publications

Processes as Predicates

Slides: Private Names in Non-Commutative Logic

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.

A technical report contains the details of the cut elimination proof.

Session Types

Slides: Designing, Verifying and Monitoring Protocols inspired by Scribble.

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. Our approach follows a propositions-as-processes style, hence is distinct from the logical characterisation of multi-party compatibility in a proofs-as-processes style developed independently and published simultaneously by Carbone et al..

Web of Linked Data

26/2/2016: The second of two journal papers on RDF Schema from the perspective of type systems is accepted for publication in Journal of Logical and Algebraic Methods in Programming. These two papers represent a mature line of work that is ready to be implemented by a graduate student interested in making data on the Web easier to consume.

Gabriel Ciobanu, Ross Horne, and Vladimiro Sassone. Minimal type inference for Linked Data consumers. Journal of Logical and Algebraic Methods in Programming 84.4 (2015): 485-504. DOI:10.1016/j.jlamp.2014.12.005

Gabriel Ciobanu, Ross Horne, and Vladimiro Sassone. A descriptive type foundation for RDF Schema. Journal of Logical and Algebraic Methods in Programming 85.5 (2016): 681-706. DOI:10.1016/j.jlamp.2016.02.006

The two journal papers on RDF Schema types are summarised in the audio slides on this page. The slides, without audio, are also available.

The first of the two papers provides a gentle introduction to consuming data on the Web called Linked Data and introduces a simple scripting language, with a conventional "prescriptive" type system, that makes the consumer's life easier.

The second of the two papers addresses more challenging aspects of RDF Schema types. The paper introduces a novel "descriptive" type system that evolves to describe data discovered at run-time by the Linked Data consumer. The descriptive type system can adapt to several modes of inference ranging from W3C standard compliant RDF Schema inference to something more accommodating. When the descriptive type system is unsure about the appropriate mode of inference, a warning with a menu of options is generated for the consumer reflecting the subjective nature of knowledge published on the Web.

Developing Research in Computer Science

Previously, since 2012, I was associate professor at Kazakh-British Technical University and a research associate at Romanian Academy.

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 certified 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.

I am a European. I believe passionately that our doors should be open to everyone.
Mail me at: