About

I am a Senior Lecturer in the department of Computer and Information Sciences at the University of Strathclyde. I am a member of the department’s Mathematically Structured Programming (MSP) group.

My research is on programming languages. I use mathematical ideas and structure from logic, category theory, type theory, and denotational semantics to study programming languages and the systems they describe.

Recent Posts

• 2023-11-02: More Data Types with Negation at Fun in the REPL
• 2023-01-17: Compiling higher-order specifications to SMT solvers
• 2023-01-16: Simple semantics for defaults in Catala
• 2023-01-15: Data types with Negation
• 2020-11-23: Slides and Video for “Resource Constrained Programming with Full Dependent Types”

See also all posts sorted by year or the RSS feed.

Publications

See also DBLP or Google Scholar.

• Polynomial Time and Dependent Types
  POPL 2024
• A Semantic Proof of Generalised Cut Elimination for Deep Inference
  MFPS LX, 2024
• Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
  CPP 2023
• Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
  ArXiv 2022
• A Framework for Substructural Type Systems
  ESOP 2022
• Data types with Negation (Talk Abstract)
  MSFP 2022 (Talk Abstract)
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
  Journal of Functional Programming 2021
• A Linear Algebra Approach to Linear Metatheory
  Linearity-TLLA 2020
• Effect Handlers via Generalised Continuations
  Journal of Functional Programming, 2020
• Dijkstra Monads for All
  ICFP 2019
• Context Constrained Computation
  TyDe 2018 (Extended Abstract)
• A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
  ICFP 2018
• The Syntax and Semantics of Quantitative Type Theory
  LICS 2018
• Compiling Parallel Functional Code with Data Parallel Idealised Algol
  ArXiv (2017)
• Observed Communication Semantics for Classical Processes
  ESOP 2017
• Continuation Passing Style for Effect Handlers
  FSCD 2017
• Conflation Confers Concurrency
  WadlerFest 2016
• Interleaving data and effects
  Journal of Functional Programming, 2015
• Models for Polymorphism over Physical Dimensions
  TLCA 2015
• ThreadSafe: Static Analysis for Java Concurrency
  AVoCS 2015
• From Parametricity to Conservation Laws, via Noether's Theorem
  POPL 2014
• A Relationally Parametric Model of Dependent Type Theory
  POPL 2014
• Abstraction and Invariance for Algebraically Indexed Types
  POPL 2013
• Productive Coprogramming with Guarded Recursion
  ICFP 2013
• Refining Inductive Types
  Logical Methods in Computer Science, 2012
• Fibrational Induction Meets Effects
  FoSSaCS 2012
• The Semantics of Parsing with Semantic Actions
  LICS 2012
• Relational Parametricity for Higher Kinds
  CSL 2012
• Amortised Resource Analysis with Separation Logic
  Logical Methods in Computer Science, 2011
• When Is a Type Refinement an Inductive Type?
  FoSSaCS 2011
• Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode
  TGC 2010
• Amortised Resource Analysis with Separation Logic
  ESOP 2010
• Parameterised notions of computation
  Journal of Functional Programming, 2009
• A Deep Embedding of Parametric Polymorphism in Coq
  WMM 2009
• Unembedding domain-specific languages
  Haskell Symposium 2009
• Syntax for Free: Representing Syntax with Binding Using Parametricity
  TLCA 2009
• Algebras for Parameterised Monads
  CALCO 2009
• What is a Categorical Model of Arrows?
  MSFP 2008
• Secure Execution of Mobile Java using Static Analysis and Proof Carrying Code
  UK e-Science AHM 2007
• CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
  TYPES 2007
• Specifying and Verifying Heap Space Allocation with JML and ESC/Java2
  FTfJP 2006
• Substructural Simple Type Theories for Separation and In-place Update
  PhD Thesis
• Parameterised Notions of Computation
  MSFP 2006
• A 𝜆-Calculus for Resource Separation
  ICALP 2004