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

Research staff

Alex Smith

Honorary research fellows

Valeria de Paiva

Reinhold Heckmann

Claudio Hermida

Paul Taylor

PhD Students

Student Supervisor
Michael ArntzeniusNeel Krishnaswami
Auke BooijMartín Escardó
Yuning FengPaul Levy
Bram GeronPaul Levy
Sina HazratpourSteve Vickers
Tomáš JaklAchim Jung and Aleš Pultr (Charles University in Prague)
Xiaodong JiaAchim Jung
Cory KnappMartín Escardó