People
The group was set up on 1st July 2008 within the Department of Computer and Information Sciences at the University of Strathclyde.
Academic Staff
who is currently working on theories of advanced data types, containers, induction recursion, parametricity and all areas of category theory. See Neil's webpage or email neil.ghani@strath.ac.uk.
who is currently working on dependently typed programming. They are also interested in extending the functionality of Haskell so that it can mimic the dependently typed style of programming. See Conor's webpage or email conor.mcbride@strath.ac.uk.
who is currently working on both coalgebras and logics for knowledge representation, learning and verification. See Clemens's webpage or email clemens.kupke@strath.ac.uk.
who is currently working on mixing linear and dependent types, and development of safe and verified AI. See Bob's webpage or email robert.atkey@strath.ac.uk.
who is interested in Martin-Löf Type Theory, constructive mathematics, and category theory. See Fredrik's webpage or email fredrik.nordvall-forsberg@strath.ac.uk.
who is interested in efficient runtime representations, generic programming, proof automation, and user experience. See Guillaume's webpage or email guillaume.allais@strath.ac.uk.
who is interested in concurrency and logic, and their applications to verifying the security and privacy or protocols. See Ross's webpage or email ross.horne@strath.ac.uk.
who is interested in dependent types, type theory and programming language design and their application in making systems more trustworthy. See Jan's webpage or email jan.de-muijnck-hughes@strath.ac.uk.
PhD Students
who is a PhD student under Conor McBride's direction. See Stuart's webpage.
who is a PhD student under Clemens Kupke's direction.
who is a PhD student under Clemens Kupke's and Neil Ghani's direction.
who is a PhD student under Conor McBride's direction. See Malin's webpage.
who is a PhD student under Fredrik Nordvall Forsberg's direction.
who is a PhD student under Neil Ghani and Scott Cunningham's direction. See Matteo's webpage.
who is a PhD student under Radu Mardare and Neil Ghani's direction. See Eigil's webpage.
who is a PhD student under Bob Atkey and Conor McBride's direction. See Andre's webpage.
who is a PhD student under Clemens Kupke's direction.
who is a PhD student under Jules Hedges' direction. See Dylan's webpage.
who is a PhD student under Clemens Kupke and Fredrik Nordvall Forsberg's direction. See Sean's webpage.
who is a PhD student under Conor McBride and Viv Kendon's direction.
who is a PhD student under Bob Atkey's direction. See April's webpage.
who is a PhD student under Fredrik Nordvall Forsberg's direction.
who is a PhD student under Jules Hedges' direction. See Fiona's webpage.
who is a PhD student under Guillaume Allais' direction.
Alumni
who was a Chancellor's Fellow working on game theory, economics and machine learning using the tools of category theory and functional programming. See Jules's webpage.
who was a PhD student under Jules Hedges' direction. Riu successfully defended his thesis "Categorical Models in Control Theory and Reinforcement Learning" in July 2025, with Fabio Zanasi as external examiner and Bob Atkey as internal. See Riu's webpage.
who was an RA working with Clemens Kupke. See Clovis's webpage.
who worked on mathematical models of interaction such as distributed games and event structures.
who is interested in mathematical tools for modelling and reasoning about systems, especially in the use of metric spaces for quantitative and probabilistic reasoning. See Radu's webpage.
who is interested in dependent types, linear types and other substructural friends, lightweight verification, and verification of machine learning. See Wen's webpage.
who worked on modelling infectious diseases using tools such as stochastic graph rewriting and evolutionary game theory.
who is interested in the compositionality of formal verification and programming within a coalgebraic framework. See Jade's webpage.
who was a PhD student under Ross Duncan's direction. Joe successfully defended his thesis "Hopf-Frobenius Algebras" in January 2024, with Chris Heunen as external examiner, and Jules Hedges as internal.
who was a PhD student under Bob Atkey's direction. James passed his viva in January 2024 with external examiner Kathrin Stark, and internal examiner Conor McBride. His thesis is entitled "A Framework for Semiring-Annotated Type Systems". See James's webpage.
who worked as a Research Software Engineer in the group.
who was a PhD student under Neil Ghani's direction. Bruno's thesis, successfully defended 2023, is entitled "Fundamental components of deep learning: a category-theoretic approach". See Bruno's webpage.
who is interested in concurrency, topology, epistemic logic and category theory. See Jérémy's webpage.
who was a KTP Associate at Cambridge Quantum Computing under Conor McBride and Ross Duncan's direction.
who is interested in quantum computation, the foundations of quantum mechanics, category theory and its application in computer science, logic and physics, and graphical techniques for reasoning.
who was a KTP Associate at Symphonic Software under Bob Atkey's direction.
who was a PhD student under Conor McBride's direction.
who was a PhD student under Conor McBride's direction.
who was a PhD student under Ross Duncan's direction on the topic of categorical semantics of quantum physics.
who worked as an RA on Neil Ghani and Conor McBride's grant Homotopy Type Theory: Programming and Verification. See James's webpage.
who worked as an RA on Clement Kupke's grant Coalgebraic Foundations of Semi-Structured Data. See Johannes's webpage.
who was a PhD student under Neil Ghani's direction on the topic of bifibrational parametricity.
who was a PhD student under Clemens Kupke's direction. See Alwin's webpage.
who was a PhD student under Neil Ghani's direction on the topic of symmetry and parametricity. See Tim's webpage.
who was a PhD student under Neil Ghani's direction on the topic of induction-recursion.
who is interested in logic, type theory and computer systems. He worked with Prof. Neil Ghani on induction recursion. See Peter G.'s webpage.
was a PhD student under Patricia Johann's direction on the topic of generic induction principles. Clément completed his PhD in 2012. Clément's thesis is entitled "Induction and Coinduction schemes in Category Theory". His examiners were Bart Jacobs (external) and Conor McBride.
who worked on advanced data types and categorical and operational models of parametricity. Patricia left in 2013 to take up a Chair at Appalachian State University. See Patricia's webpage.
who worked as an RA on Dr McBride's grant Haskell Types with Added Value. See Sam's webpage.
who was a PhD student under Conor McBride's direction on the topic of reusability and dependent types. See Pierre-Evariste's webpage.
who was a PhD student under Conor McBride's direction on the topic of adding Nat-indexed families to Haskell. See Adam's webpage.