Ross Horne

I summarise key results and research directions.

Equivalence checking and privacy. In my previous post as senior research fellow at Nanyang Technological University, Singapore, we solved several problems in protocol verification which use logic to give us a better understanding of congruences for process calculi [CONCUR'17, LICS'18, LMCS'21, ICTAC'21]. These breakthroughs enable us to refine methoods for verifying privacy properties using cryptographic calculi. The methodology was used to discover a privacy vulnerability for ePassports [ESORICS'19, LMCS'21].

Linked Data. My PhD thesis at University of Southampton was on high-level languages for consuming data published on the Web. Such language abstractions [Sci.Comp.Prog.'14, JLAMP'15, JLAMP'16] allow programs to engage in sessions, where information discovered in queries can be used to form new queries, thereby navigating an interlinked Web of Data. Providing high-level language abstractions makes such programming tasks easier. This led me to the notion of a descriptive type system, which assists the data consumer during such interactions by generating suggestions for how inconsistencies in data may be resolved.

On session types and proof theory. I have proposed a proof theoretic approach to multi-party session types [PSI'15, SACS'15, CONCUR'20, TCS'20]. This work perhaps challenges the culture of type theorists, who, at times, may equate proof theory for types with the Curry-Howard correspondence. While the Curry-Howard correspondence is a remarkable achievement; my message to the session type community is that structural proof theory has much more to offer. I explain this in a video presented at CONCUR'20.

Attack trees. Attack trees, employed for security assessment, are also amenable to proof theoretic techniques [Fund.Inf.'16, GramSec'18, GramSec'20]. This is natural, since there are explanations of the logical systems in terms of game semantics and argumentation, which account for tensions between an attacker and defender competing on an attack surface.

Education

• Doctor of Philosophy (Ph.D.) University of Southampton (2007 — 2011)
• MA University of Oxford (2001 — 2005)
• Secondary Education Kelso High School (1996 — 2001)

Companies

• Research Fellow University of Luxembourg (2018)
• Senior Research Fellow Nanyang Technological University, Singapore (2015 — 2018)
• Research Associate Romanian Academy (2012 — 2016)
• Associate Professor Kazakh-British Technical University (2012 — 2016)
• Visiting Professor Suleyman Demirel University, Kazakhstan (2015 — 2015)
• Assistant Professor Kazakh-British Technical University (2012 — 2012)
• Software Engineer Calligrafix (2001 — 2003)