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.



 Research areas
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
Neel Krishnaswami
type theory, verification, substructural logic, interactive computation
Paul Levy denotational semantics, λ-calculus with effects,
nondeterminism, category theory, game semantics
Uday Reddy semantics of state, separation logic
Eike Ritter security protocol verification
Hayo Thielecke abstract machines, concurrent and functional programming, software security
Steve Vickers constructive mathematics and topology, category theory and toposes

PhD Students

Student Supervisor
Olle FredrikssonDan Ghica
Bram GeronPaul Levy
Tomáš JaklAchim Jung and Aleš Pultr (Charles University in Prague)
Xiaodong JiaAchim Jung and Qingguo Li (Hunan University)
Cory KnappMartín Escardó
Asiri RathnayakeHayo Thielecke
Alex SmithDan Ghica
Chuangjie XuMartín Escardó
Zhongxi ZhangMartín Escardó and Qingguo Li (Hunan University)