Ross Horne

Senior lecturer in cyber security: ross.horne@strath.ac.uk

I'm a senior lecturer in the department of Computer & Information Sciences at University of Strathclyde, Glasgow, United Kingdom. I'm a member of the Strathclyde Cyber Security (StrathCyber) and the Mathematically Structured Programming (MSP) research groups.

Selected security and privacy research

Private contactless payments

November 2023: The EMV protocol that you use to make payments using cards and phones has several privacy limitations. An eavesdropper can intercept cleartext messages containing personally identifiable information on the air, hence this information is encrypted in EMV Kernel 8, released in 2023. However, that new protocol does not counter threats where an active attacker in proximity to the user initiates a session with a contactless card. We propose a protocol that does counter such threats and related challenges such as data minimisation.

An extended version of the paper is available on arXiv, details of proofs that establish unlinkability with respect to different threats and data minimisation goals. See also the PhD thesis of Semen Yurkov for further background on the problem.

July 2022: We have analysed the key agreement propose for what is now EMV Kernel 8. By taking into account active attackers, who can activate a card, we show that a card holder can be tracked using the certificate presented. We present and verify a solution where self-blinding certificates are used so that unlinkability holds while the terminal can authenticate that the card was issued by a trusted payment system.

ePassport unlinkability

September 2019: Our papers presented at ESORICS 2019 and communicated in LMCS report on a privacy vulnerability in the ICAO 9303 standard used by ePassports. The vulnerability allows an individual who has recently passed through a passport control point to be re-identified, even without opening their passport.

Here are the slides presented at ESORICS 2019. Also we have a repository providing practical evidence for the vulnerability and the following video (featuring Ihor Filimonov, Zach Smith, Sevdenur Baloglu, and Husam Al-Jawaheri) suggesting how the vulnerability may be exploited.

Note, for this proof of concept, this demonstration uses phones but an attacker may use more discrete and powerful devices.

Responsible disclosure: The vulnerability has been reported to ICAO, along with our recommendation for how ePassport readers may mitigate the vulnerability. ICAO issued a public response both confirming the vulnerability and reassuring the public that the scope of the vulnerability is limited. Their response was reported in Delano magazine and Paperjam.

The press release on this privacy vulnerability was also reported in news outlets including the Luxembourg Times , the Luxemburger Wort , and the magazine of FNR: science.lu. The resulting public interest caused a motion to be submitted to the Luxembourg parliament, leading to a joint response from the prime minister Xavier Bettel and foreign affairs minister Jean Asselborn. The vulnerability was also reported on the 100komma7 radio station and RTL TV stations. The video from RTL (in Luxembourgish) is reproduced below.

Verifiable credentials

April 2024: Verifiable credentials can be used for authentication. The verifiable credential is issued by a trusted authority to the holder and the holder presents the credential to an entity with whom they wish to authenticate. That whole process should follow a protocol, which we define and prove resilient to various threats.

Chinese wall security policy models

July 2024: The Brewer-Nash security policy model was introduced by Brewer and Nash in 1989 and is one of the most influential papers in computer security. It is a model of how Chinese walls are used to avoid conflicts of interest between organisations. For example, a consultant should never posses confidential information about two companies that are separated by a conflict of interest. A distinguishing feature of such policies is that what can be read and writen evolves dynamically and hence access is based on the current state, not only the conflicts of interest that are present. Notably write access may be revoked after reading certain confidential information to maintain confidentiality.

Causal Attack Trees and Attack-Defence Frameworks

November 2020: We have a position paper on argumentation-based semantics for attack-defence trees. Argumentation, arising from the systematisation of conflict in legal arguments, and attack-defence tree, inspired by fault trees, are both based on around 50 years of research. They have obvious parallels, since both deal symbolically with conflict, cooperation and competition, that we draw attention to here. The semantics we propose combines several models of argumentation in a new way, permitting more flexible generalisations of attack-defence trees. An argumentation-based semantics can be used to turn attack trees into decision making mechanisms, which means that it plays quite a different role from the semantics of attack trees that preserve attribute domains.

March 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".

Slides: Specialisation of Attack Trees with Sequential Refinement

A supporting technical report includes proofs omitted from the journal version.

The game semantics behind such attack trees is explored in a paper presented at GraMSec'18. We emphasise the difference between when an attacker making a choice and when the environment or defender makes a choice in an attack scenario.

Selected research on concurrency theory, proof theory, space, and knowledge graphs

Session Types

June 2021: There are many fairness assumptions to chose from when verifying liveness properties. In this paper, communicated at LICS'21, we systematically investigate how fairness assumptions impact a liveness property targeted by session type systems, called lock-freedom. We identify one particular notion of fairness, called justness, that gives rise to "just lock-freedom" which is the tightest match for session types.

The slides are available here.

I have a series of papers on multiparty session types employing analytic proof calculi developed using methods from structural proof theory:

These papers present a purely logical approach to a rich multiparty subtype system that also captures multiparty compatibility. The videos lectures presented at CONCUR 2020 explain the connections with proof theory and provide a compelling real-world example.

There are also older slides from 2015: Designing, Verifying and Monitoring Protocols inspired by Scribble.

Analytic Proof Calculi on Graphs

July 2020. In logic we are accustomed to reasoning about formulae. Even graphical syntax (e.g., co-graphs, knowledge graphs and argumentation frames) is typically graphical representations of formulas. In this work we prove that it is possible to design a logical systems where we reason about more general graphs with an expressive power beyond that which can be expressed using formulas. This initial study focusing on a minimal setting in which we generalise conjunction and disjunction. This method will enable us to build additional expressive power into various logics, while retaining computational properties of proofs (analyticity).

Here are two videos presented at LICS 2020.


Video above: an informal chat on logic beyond formulas.

Video above: a long (uncool) presentation, explaining details to experts.

Open Bisimilarity is Intuitionistic

September 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'').

March 2018: Follow up papers, presented at LICS 2018, explains why 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 intuitionistic, but private information is treated 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.

May 2023: A paper published in Theoretical Computer Science journal explains how the technique (quasi-open bisimilarity) lifts to the full applied π-calculus. Lifting to the applied π-calculus, makes it possible to apply our methodology in order to verify privacy properties of real-world cryptographic protocols. A preliminary version appeared in ICTAC 2021.

A video of the presentation at ICTAC'21 by Semen Yurkov is available here:

Space Law and AI

CubeSat Lab experimental setup

July 2023: I was involved in setting up an Interdisciplinary Master Program in Space Resources. By taking an interdisciplinary perspective to space, I ended up interacting with various interesting people including space lawyers, leading to the following paper.

The above paper led to an ongoing project with ESA on onboard AI for improving the reliability of satellites. The results are published in the Journal of Aerospace Information Systems.

We also have the following papers on removing clouds from satellite images. This was the leading case study in a master course introducing space professionals to computer science and data science. This is published in the International Journal of Remote Sensing.

Processes as Formulae

September 2019: A series of papers on logical systems for process calculi has been published in the proceedings of CONCUR 2016, FSCD 2019 and in the journals TOCL and MSCS. These papers introduce new logical systems, directly embedding various process calculi, not limited to Robin Milner's famous π-calculus. To model private names in the π-calculus, the trick is to decompose established self-dual nominal quantifiers into a De Morgan dual pair of nominal quantifiers. We use Cyrillic vowels И and Э, pronounced `new' and `wen' respectively, for our pair of nominal quantifiers.

Slides CONCUR'16: Private Names in Non-Commutative Logic

Slides FSCD'19: The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic.

The paper published in Mathematical Structures in Computer Science develops proof normalisation techniques allowing us to extract executions of processes from proofs. We prove that linear implication is strictly finer than established weak simulation preorders (and hence probabilistic may testing). The technique lifts to a range of process calculi, not only the π-calculus.

The paper published in FSCD'19 shows that the techniques extend to probabilistic choice and probabilistic simulation. To achieve this we introduce the (probabilistic) sub-additives --- logical operators which lie between conjunction and disjunction that forbid weakening.

Web of Linked Data

June 2023: I hosted a COST workshop discussing privacy issues in distributed social knowledge graphs. This is part of an EU COST Action on Distributed Knowledge Graphs, for which I represent Luxembourg. This led to a paper where we evaluate the Solid protocol with respect security and privacy properties. The Solid protocol aims to decouple apps from storage, called Solid pods, allowing data subjects to provide their own storage for apps and thereby take sovereignty of their own data. Since personal data is involved the legal context is important, and hence we found our privacy analysis in the relevant legal obligations.

February 2016: The second of two journal papers on RDF Schema from the perspective of type systems is published 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.

The first of the two papers above 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.

First part on prescriptive types.

Second part on descriptive types.

The slides are available.

Background and Contacts

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.

From 2015 to 2023, I was a member of the "Security and Trust of Software Systems" group at University of Luxembourg and a senior research fellow in the Cyber Security Lab at Nanyang Technological University Singapore. From 2012 to 2016, I was associate professor at Kazakh-British Technical University and a research associate at Romanian Academy.

I have had the honour and pleasure to collaborate with Matteo Acclavio, Ki Yung Ahn, Bogdan Aman, Hamed Arshad, Clément Aubert, Bart Buelens, Christoph Braun, Biagio Boi, Alfredo Capozucca, Ilaria Castellani, Gabriel Ciobanu, Marco Crepaldi, Maximiliano Cristiá, Mariangiola Dezani-Ciancaglini, Christian Esposito, Ihor Filimonov, Ellie Forsyth, Dov M. Gabbay, Elfi Goesaert, Paola Giannini, Nicholas Gibbins, Reynaldo Gil-Pons, Rob van Glabbeek, Olaf Hartig, Cengis Hasan, Peter Höfner, Christian Johansen, Tobias Käfer, Ricardo Katz, Shang-wei Lin, Ben MacDonald, Sjouke Mauw, Andrzej Mizera, Livio Robaldo, Luca Padovani, Vladimiro Sassone, Zach Smith, Lutz Straßburger, André Stemper, Chang Sun, Alwen Tiu, Jan Thoemel, Leon van der Torre, Rolando Trujillo, Timur Umarov, Olaf Uwe, Cristian Văideanu, Tim Willemse, and Semen Yurkov. I look forward to future collaborations.

Selected Publications

  • 2024:
    1. SSI, from Specifications to Protocol? Formally Verify Security!. C. Braun, R. Horne, T. Käfer, and S. Mauw. In WWW '24: Proceedings of the ACM on Web Conference 2024, pp. 1620-1631, 2024. [  doi:10.1145/3589334.3645426 ]
    2. Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation. A. Capozucca, M. Cristiá, R. Horne, and R. Katz. In 37th IEEE Computer Security Foundations Symposium July 8-12, 2024 - Enschede, The Netherlands. 2024. [  preprint |  ]
    3. XACML2mCRL2: Automatic transformation of XACML policies into mCRL2 specifications. H. Arshad, R. Horne, C. Johansen, O. Owe, T.A.C. Willemse. Science of Computer Programming, Volume 232, 103046, 2024. [ doi:10.1016/j.scico.2023.103046 ]
  • 2023:
    1. Provably Unlinkable Smart Card-based Payments. S. Bursuc, R. Horne, S. Mauw and S. Yurkov. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS '23), November 26-30 2023, Copenhagen, Denmark. ACM, New York, NY, USA, 15 pages. 2023. [  preprint | doi:10.1145/3576915.3623109 ]
    2. Assessing the Solid Protocol in Relation to Security and Privacy Obligations. C. Esposito, R. Horne, L. Robaldo, B. Buelens and E. Goesaert. Information, 14(7), 2023. [ preprint | doi:10.3390/info14070411 ]
    3. Anomaly detection using deep learning respecting the resources on board a CubeSat. R. Horne, S. Mauw, A. Mizera and J. Thoemel. Journal of Aerospace Information Systems, 2023. [ doi:10.2514/1.I011232 ]
    4. A Logical Account of Subtyping for Session Types. R. Horne and L. Padovani. In Proceedings 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES@ETAPS 2023, Paris, France, 22 April 2023. EPTCS 378, pp. 26–37, 2023. [ preprint | doi:10.4204/EPTCS.378.3 ]
    5. When privacy fails, a formula describes an attack: A complete and compositional verification method for the applied π-calculus. R. Horne, S. Mauw and S. Yurkov. Theor. Comput. Sci., 959:113842, 2023. [ preprint | doi:10.1016/j.tcs.2023.113842 ]
    6. Software Certification as a Limit on Liability: the Case of Cubesat Operations. M. Crepaldi, R. Horne and S. Mauw. In Space Law in a Networked World, Brill, Studies in Space Law 19, pp. 162-186, 2023. [ preprint | doi:10.1163/9789004527270_008 ]
  • 2022:
    1. Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus. C. Aubert, R. Horne and C. Johansen. In 33rd International Conference on Concurrency Theory (CONCUR 2022) 12-16 September, Warsaw, Poland. LIPIcs, pp. 30:1–30:26, 2022. [ DOI ]
    2. Bisimulations Respecting Duration and Causality for the Non-interleaving Applied π-Calculus. C. Aubert, R. Horne and C. Johansen. In Proceedings Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics (EXPRESS⁄SOS 2022), Warsaw, Poland, 12th September 2022. Electronic Proceedings in Theoretical Computer Science 368, pp. 3–22, 2022. [ DOI ]
    3. A Graphical Proof Theory of Logical Time. M. Acclavio, R. Horne, S. Mauw and L. Straßburger. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs) 228, pp. 22:1–22:25, 2022. [ DOI ]
    4. Is Eve nearby? Analysing protocols under the distant-attacker assumption. R. Gil-Pons, R. Horne, S. Mauw, A. Tiu and R. Trujillo. In IEEE Computer Security Foundations Symposium 2022 (CSF2022), August, 2022, Haifa, Israel. pp. 17-32, 2022. [ preprint | DOI ]
    5. Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments. R. Horne, S. Mauw and S. Yurkov. In IEEE Computer Security Foundations Symposium 2022 (CSF2022), August, 2022, Haifa, Israel. pp. 364-379, 2022. [ preprint | DOI ]
    6. Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2. H. Arshad, R. Horne, C. Johansen, O. Owe and T. Willemse. In FORTE 2022 - 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems. Springer, Lecture Notes in Computer Science 13273, 2022. [ preprint | DOI ]
    7. Theories of life and computation: Special issue on the occasion of the 65th birthday of Professor Gabriel Ciobanu. 2022. [ DOI ]
    8. An Analytic Propositional Proof System on Graphs. M. Acclavio, R. Horne and L. Straßburger. Logical Methods in Computer Science, 18(4):1:1–1:80, 2022. [ preprint | DOI ]
    9. Cloud Removal from Satellite Imagery using Multispectral Edge-filtered Conditional Generative Adversarial Networks. C. Hasan, R. Horne, S. Mauw and A. Mizera. International Journal of Remote Sensing, 43(5):1881-1893, 2022. [ DOI ]
  • 2021:
    1. Compositional Analysis of Protocol Equivalence in the Applied π-Calculus Using Quasi-open Bisimilarity. R. Horne, S. Mauw and S. Yurkov. In Theoretical Aspects of Computing – ICTAC 2021. Springer International Publishing, pp. 235–255, 2021. [ DOI ]
    2. Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom. R.J. van Glabeek, P. Höfner and R. Horne. In 36th Annual ACM⁄IEEE Symposium on Logic in Computer Science (LICS ’21). IEEE, pp. 1-16, 2021. [ preprint | DOI ]
    3. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. K. Ahn, R. Horne and A. Tiu. Logical Methods in Computer Science, 17(3):2:1–2:40, 2021. [ preprint | DOI ]
    4. Discovering ePassport Vulnerabilities using Bisimilarity. R. Horne and S. Mauw. Logical Methods in Computer Science, 17(2):24:1–24:52, 2021. [ preprint | DOI ]
  • 2020:
    1. Attack-Defence Frameworks: Argumentation-Based Semantics for Attack-Defence Trees. D.M. Gabbay, R. Horne, S. Mauw and L. van der Torre. In Graphical Models for Security - 7th International Workshop, GraMSec 2020, Boston, MA, USA, June 22, 2020 Revised Selected Papers. Springer, Lecture Notes in Computer Science 12419, pp. 143–165, 2020. [ preprint | DOI ]
    2. Session Subtyping and Multiparty Compatibility Using Circular Sequents. R. Horne. In 31st International Conference on Concurrency Theory (CONCUR 2020). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs) 171, pp. 12:1–12:22, 2020. [ preprint | DOI ]
    3. Logic Beyond Formulas: A Graphical Proof System. M. Acclavio, R. Horne and L. Straßburger. In 35th Annual ACM⁄IEEE Symposium on Logic in Computer Science (LICS '20), July 8-11, 2020, Saarbrücken, Germany. ACM, pp. 15, 2020. [ preprint | DOI ]
    4. Global types with internal delegation. I. Castellani, M. Dezani-Ciancaglini, P. Giannini and R. Horne. Theoretical Computer Science, 807:128 - 153, 2020. [ preprint | DOI ]
  • 2019:
    1. Graphical Models for Security - 6th International Workshop, GraMSec@CSF 2019, Hoboken, NJ, USA, June 24, 2019, Revised Papers. M. Albanese, R. Horne and C.W. Probst, editors. Lecture Notes in Computer Science 11720, 2019. [ preprint | DOI ]
    2. Breaking Unlinkability of the ICAO 9303 Standard for e-Passports Using Bisimilarity. I. Filimonov, R. Horne, S. Mauw and Z. Smith. In Computer Security – ESORICS 2019. Springer International Publishing, pp. 577–594, 2019. [ preprint | DOI ]
    3. The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic. R. Horne. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019).. LIPIcs, pp. 23:1–23:16, 2019. [ preprint | DOI ]
    4. De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic. R. Horne, A. Tiu, B. Aman and G. Ciobanu. ACM Transactions in Computational Logic (TOCL), 20(4):22:1–22:44, 2019. [ preprint | DOI ]
    5. Constructing Weak Simulations from Linear Implications for Processes with Private Names. R. Horne and A. Tiu. Mathematical Structures in Computer Science, 29(8):1275-1308, 2019. [ preprint | DOI ]
  • 2018:
    1. The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement. R. Horne, S. Mauw and A. Tiu. In Graphical Models for Security. Springer International Publishing, pp. 90–110, 2018. [ preprint | DOI ]
    2. Quasi-Open Bisimilarity with Mismatch is Intuitionistic. R. Horne, K. Ahn, S. Lin and A. Tiu. In In Proceedings of LICS ’18: 33rd Annual ACM⁄IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS ’18). pp. 26-35, 2018. [ preprint | DOI ]
  • 2017:
    1. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. K. Ahn, R. Horne and A. Tiu. In 28th International Conference on Concurrency Theory (CONCUR 2017).. Leibniz International Proceedings in Informatics 85, pp. 7:1-7:17, 2017. [ preprint | DOI ]
    2. Semantics for Specialising Attack Trees based on Linear Logic. R. Horne, S. Mauw and A. Tiu. Fundamenta Informaticae, 153(1-2):57-86, 2017. [ preprint | DOI ]
  • 2016:
    1. Private Names in Non-Commutative Logic. R. Horne, A. Tiu, B. Aman and G. Ciobanu. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics, pp. 31:1-31:16, 2016. [ preprint | DOI ]
    2. A descriptive type foundation for RDF Schema. G. Ciobanu, R. Horne and V. Sassone. Journal of Logical and Algebraic Methods in Programming, 85(5):681-706, 2016. [ preprint | DOI ]
    3. SPEC: An Equivalence Checker for Security Protocols. A. Tiu, N. Nguyen and R. Horne. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings. Lecture Notes in Computer Science 10017, pp. 87–95, 2016. [ DOI ]
  • 2015:
    1. The consistency and complexity of multiplicative additive system virtual. R. Horne. Scientific Annals of Computer Science, 25(2):245-316, 2015. [ preprint | DOI ]
    2. Behavioural analysis of sessions using the calculus of structures. G. Ciobanu and R. Horne. In 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. Springer, LNCS 9609, pp. 91-106, 2015. [ bib | preprint | DOI ]
    3. Minimal type inference for Linked Data consumers. G. Ciobanu, R. Horne and V. Sassone. Journal of Logical and Algebraic Methods in Programming, 84(4):485-504, 2015. [ preprint | DOI ]
    4. Embracing Global Computing in Emerging Economies - First Workshop, EGC 2015, Almaty, Kazakhstan, February 26-28, 2015. Proceedings. R. Horne, editor. Communications in Computer and Information Science 514, 2015. [ DOI ]
  • 2014:
    1. A verified algebra for read-write Linked Data. R. Horne and V. Sassone. Sci. Comput. Program., 89:2–22, 2014. [ DOI ]
  • 2013:
    1. Non-interleaving Operational Semantics for Geographically Replicated Databases. G. Ciobanu and R. Horne. In 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, September 23-26, 2013. IEEE Computer Society, pp. 440–447, 2013. [ DOI ]
  • 2012:
    1. Tracing where and who provenance in Linked Data: A calculus. M. Dezani-Ciancaglini, R. Horne and V. Sassone. Theor. Comput. Sci., 464:113–129, 2012. [ DOI ]
  • 2011:
    1. Operational Semantics for SPARQL Update. R. Horne, V. Sassone and N. Gibbins. In The Semantic Web - Joint International Semantic Technology Conference, JIST 2011, Hangzhou, China, December 4-7, 2011. Proceedings. Springer, Lecture Notes in Computer Science 7185, pp. 242–257, 2011. [ DOI ]

Office telephone: +44 141 548 3397. Address: Livingstone Tower, floor 14, office 1402a. 26 Richmond St, Glasgow G1 1XH