Overview
Our work concerns the development and study of precise mathematical formalisms that can be employed for the design, specification, and verification of computer programs. This is in a tradition of mathematical semantics that was started in the UK in the 1960s by Peter Landin, Christopher Strachey, and Dana Scott. This kind of semantics encompasses many mathematical theories, foremost among them order theory, topology, logic, game theory, and category theory, all of which feature in the work of the Birmingham Theory Group. The rich and often surprising interplay between these mathematical areas and programming concerns gives rise to wonderful opportunities for deep and conceptual research.
PhD opportunities
See our poster here.
We welcome applicants for PhD studies in any of these areas. Please email for more information, or contact individual researchers.
Staff
Research areas  
Benedikt Ahrens 
semantics of type theory, computer theorem proving, categorical structures in programming 

Martín Escardó 
topology, computation with infinite objects, constructive mathematics, intuitionistic type theory 

Dan Ghica  game semantics, heterogeneous computing, model checking  
Achim Jung  mathematical structures in the foundations of computing: logic, topology, order  
Paul Levy 
denotational semantics, computational effects and callbypushvalue, nondeterminism, category theory, coalgebra, game semantics  
Dave Parker  formal verification, probabilistic model checking  
Uday Reddy  semantics of state, separation logic  
Eike Ritter  security protocol verification  
Hayo Thielecke  abstract machines, concurrent and functional programming, software security  
Jamie Vicary  quantum computing, higherdimensional algebra, category theory, quantum field theory, formal proof 

Steve Vickers  constructive mathematics and topology, category theory and toposes  
Noam Zeilberger 
categorical semantics of type systems and λcalculus, substructural logic and proof theory, interactions with combinatorics 
Research staff
Honorary research fellows
PhD Students
Student  Supervisor 
Michael Arntzenius  Dan Ghica and Neel Krishnaswami (University of Cambridge) 
Auke Booij  Martín Escardó 
Steven Cheung  Dan Ghica 
Yuning Feng  Paul Levy 
Bram Geron  Paul Levy 
Sina Hazratpour  Steve Vickers 
Tomáš Jakl  Achim Jung and Aleš Pultr (Charles University in Prague) 
Xiaodong Jia  Achim Jung 
Cory Knapp  Martín Escardó 
Koko Muroya  Dan Ghica 
Anna Laura Suarez  Achim Jung and Steve Vickers 
Seminars
 Theory seminar, usually Fridays 1112 a.m. in the Sloman Lounge
 Theory group lab lunch, usually Wednesdays 12 p.m.
 Categories reading group (CARGO) usually Tuesdays 24 p.m.
 Midlands Graduate School in the Foundations of Computing Science
 Wessex theory seminar
 Midlands logic seminar
 Departmental seminar
 Yorkshire and Midlands Category Theory Seminar (YaMCATS)