Publications

Programming Language Foundations in Agda, in collaboration with Philip Wadler and Jeremy G. Siek.

A Semantic Proof of Generalised Cut Elimination for Deep Inference, in collaboration with Robert Atkey, in Electronic Notes in Theoretical Informatics and Computer Science, December 2024.

Prioritise the Best Variation, in collaboration with Ornela Dardha, in Logical Methods in Computer Science, December 2023.

Separating Sessions Smoothly, in collaboration with Simon Fowler, Ornela Dardha, Sam Lindley, and J. Garrett Morris, in Logical Methods in Computer Science, July 2023.

Towards Races in Linear Logic, in collaboration with J. Garrett Morris and Philip Wadler, in Logical Methods in Computer Science, December 2020.

Featherweight Go, in collaboration with Robert Griesemer, Raymond Hu, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, and Nobuko Yoshida, in Proceedings of the ACM on Programming Languages, 2020.

Rusty Variation: Deadlock-free Sessions with Failure in Rust, in Electronic Proceedings in Theoretical Computer Science, September 2019.

Programming Language Foundations in Agda, in collaboration with Jeremy G. Siek and Philip Wadler, in Science of Computer Programming, August 2020.

Better Late Than Never: A fully-abstract semantics for Classical Processes, in collaboration with Fabrizio Montesi and Marco Peressotti, in Proceedings of the ACM on Programming Languages, January 2019.

Towards a Semantic Model for Textual Entailment, in collaboration with Assaf Toledo, Stavroula Alexandropoupou, Sophie Chesney, Sophia Katrenko, Heidi Klockmann, Benno Kruit, and Yoad Winter, in Perspectives on Semantic Representations for Textual Inference, 2014.

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively, in collaboration with Matthew L. Daggitt, Robert Atkey, Ekaterina Komendantskaya, and Luca Arnaboldi, in Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs.

Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks, in collaboration with Matthew L. Daggitt, Robert Atkey, Luca Arnaboldi, and Ekaterina Komendantskaya, in Proceedings of the 5th International Workshop on Formal Methods for ML-Enabled Autonomous Systems 2022.

Why Robust Natural Language Understanding is a Challenge, in collaboration with Marco Casadio, Ekaterina Komendantskaya, Verena Rieser, Matthew L. Daggitt, and Daniel Kienitz, in Proceedings 5th International Workshop, Software Verification and Formal Methods for ML-Enabled Autonomous Systems 2022.

Neural Network Robustness as a Verification Property: A Principled Case Study, in collaboration with Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Guy Katz, Guy Amir, and Idan Refaeli.

Separating Sessions Smoothly, in collaboration with Simon Fowler, Ornela Dardha, J. Garrett Morris, and Sam Lindley, in 32nd International Conference on Concurrency Theory (CONCUR 2021).

Deadlock-Free Session Types in Linear Haskell, in collaboration with Ornela Dardha, in Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell.

Prioritise the Best Variation, in collaboration with Ornela Dardha, in Proceedings of Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Msida, Malta, June 14-18, 2021.

Continuous Verification of Machine Learning: a Declarative Programming Approach, in collaboration with Ekaterina Komendantskaya and Daniel Kienitz, in 22nd International Symposium on Principles and Practice of Declarative Programming.

Neural Networks, Secure by Construction: An Exploration of Refinement Types, in collaboration with Ekaterina Komendantskaya, Daniel Kienitz, David Aspinall, and Robert Atkey, in Proceedings 18th Asian Symposium on Programming Languages and Systems, APLAS 2020, Fukuoka, Japan.

Robustness as a Refinement Type: Verifying Neural Networks in Liquid Haskell and F*, in collaboration with Ekaterina Komendantskaya, Daniel Kienitz, and David Aspinall, in 4th Workshop on Learning in Verification, Dublin, Ireland.

Taking Linear Logic Apart, in collaboration with Fabrizio Montesi and Marco Peressotti, in Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Oxford, UK, 7-8 July 2018.

Towards Races in Linear Logic, in collaboration with J. Garrett Morris and Philip Wadler, in Lecture Notes in Computer Science.

Exploring the Expressivity of Constraint Grammar, in collaboration with Inari Listenmaa, in Workshop on Constraint Grammar at NoDaLiDa’17, Gothenburg, Sweden.

Strong and Weak Quantifiers in Focused NLCL, in Logical Aspects of Computational Linguistics, Nancy, France.

Formalising Type-Logical Grammar in Agda, presented at Workshop on Type Theory and Lexical Semantics at ESSLLI’15, Barcelona, Spain.

Auto in Agda: Programming Proof Search using Reflection, in collaboration with Wouter Swierstra, in Mathematics of Program Construction, Köningswinter, Germany.

Semantic Annotation of Textual Entailment, in collaboration with Assaf Toledo, Stavroula Alexandropoulou, Sophia Katrenko, Heidi Klockmann, and Yoad Winter, in International Conference on Computational Semantics, Potsdam, Germany.

A Proof-Based Annotation Platform of Textual Entailment, in collaboration with Assaf Toledo, Stavroula Alexandropoulou, Sophie Chesney, Robert Grimm, Benno Kruit, Kyriaki Neophytou, Antony Nguyen, and Yoad Winter, in Workshop on Interoperable Semantic Annotation, Reykjavik, Iceland.

Propositions As Sessions Taken Apart, Doctoral thesis, University of Edinburgh, August 2024.

Races in Classical Linear Logic, Master’s thesis, University of Edinburgh, August 2017.

NLQ: a modular type-logical grammar for quantifier movement, scope islands, and more, Master’s thesis, Utrecht University, December 2015.

Thinning Thinning, presented at TYPES, Glasgow, UK, June 2025.

Vehicle: Bridging the Embedding Gap, presented at ARIA Research Workshop, Birmingham, UK, March 2024.

How to Talk about Youtube Radicalisation: Framing Social-Epistemological Approaches to Recommender-Driven Radicalisation, in collaboration with Lilith W. Lee, presented at Extreme Beliefs 2022, Amsterdam, NL, September 2022.

Deadlock-free Session Types in Linear Haskell, presented at Haskell Symposium 2021, Daejon, KR, August 2021.

Integrating Agda with SMT-LIB: An incomplete list of pits I fell in, presented at TyDE 2021, Daejon, KR, August 2021.

Prioritising is not my FORTE, presented at FORTE 2021, Valletta, MT, June 2021.

Robustness as a Refinement Type, presented at APLAS 2020, Fukuoka, JP, November 2020.

Verifying Neural Networks with Agda, presented at Chalmers University of Technology, Göteborg, SE, November 2020.

Session Types and Cake, presented at MFS, University of Bath, Bath, UK, November 2020.

An introduction to Session Types, presented at LSDlab, UCSC, Santa Cruz, California, October 2020.

Schmitty the Solver, presented at AIM XXXIII, Online, October 2020.

Robustness as a Refinement Type, presented at SPLS, Edinburgh, UK, July 2020.

This talk won’t help you steal, presented at CDT Pizza, Edinburgh, UK, November 2019.

Programming Programming Language Foundations in Agda in Agda, presented at AIM XXX, Munich, Germany, September 2019.

Rusty Variation: Deadlock-free sessions with failure in Rust, presented at ICE, DisCoTec, Lyngby, Denmark, June 2019.

Session Types and Cake, presented at COORDINATION, DisCoTec, Lyngby, Denmark, June 2019.

Programming Programming Language Foundations in Agda in Agda, presented at Shameless PLUG, University of Glasgow, Glasgow, UK, May 2019.

A Tale of Three Constructed Languages, presented at CDT Pizza, Edinburgh, UK, May 2019.

Formalising session-typed languages \soutwithout worries with fewer worries, presented at Workshop on Behavioural APIs, ETAPS, Prague, Czech Republic, April 2019.

Rusty Variation: Deadlock-free sessions with failure in Rust, presented at Københavns Universitet, Copenhagen, Denmark, March 2019.

Rusty Variation: Deadlock-free sessions with failure in Rust, presented at ABCD meeting, London, UK, December 2018.

Where the linear lambdas go, presented at PPar Lunch, Edinburgh, UK, November 2018.

Quantitative: Resources and Types, presented at TSPL, Edinburgh, UK, November 2018.

This talk won’t help you steal, presented at CDT Pizza, Edinburgh, UK, November 2018.

Where the linear lambdas go, presented at SPLS, Glasgow, UK, October 2018.

Where the linear lambdas go, presented at University of Kansas, Lawrence, Kansas, October 2018.

Taking Linear Logic Apart, presented at Linearity and TLLA, FLoC, Oxford, UK, July 2018.

Taking apart classical processes, presented at ABCD meeting, Edinburgh, UK, December 2017.

Programming in Agda, part 2, presented at TSPL, Edinburgh, UK, November 2017.

Programming in Agda, part 1, presented at TSPL, Edinburgh, UK, November 2017.

Session Types and Cake, presented at ICFP SRC Finalist Presentation, Oxford, UK, September 2017.

Give or take: non-determinism, linear logic, and session types, presented at SPLS, St. Andrews, UK, March 2017.

Global non-determinism with termination, presented at ABCD meeting, Edinburgh, UK, March 2017.

A bunch of things to do with NLλ, presented at LACL, Nancy, France, December 2016.

Linear Logic and the Lambda Calculus, presented at TSPL, Edinburgh, UK, November 2016.

Type Theory and NLP, presented at Colloquium CoSc, Utrecht, The Netherlands, December 2015.

Type-logical grammars in Agda, presented at TyTLeS, ESSLLI, Barcelona, Spain, August 2015.

Auto in Agda, presented at Colloquium CoSc, Utrecht, The Netherlands, June 2015.

The Banshee Labyrinth, Edinburgh, UK.

The Auld Hoose, Edinburgh, UK.

Chez Philippe, Kyōto, Japan.

村屋, Kyōto, Japan.

De Onderbroek, Nijmegen, The Netherlands.

De Bijstand, Nijmegen, The Netherlands.

Kafé België, Utrecht, The Netherlands.

ACU, Utrecht, The Netherlands.