Research Interests

Programming Languages and Systems, Verification, Semantics and Logic of Computation, Logic and Algorithms, Security, Algorithmic Game Theory.

I have worked in a wide range of areas in the semantics and logic of computation, including lambda calculus, type theory, semantics of programming languages, linear logic and computational proof theory. I have contributed to the development of game semantics, and its application to compositional software model checking and program analysis. More recently my work has focussed on higher-order model checking, a new branch of algorithmic verification that combines ideas and methods from semantics with automata-theoretic and allied techniques in automatic verification, with application to the verification of higher-order programs. I have also published in concurrency, language-based security, algorithmic game theory, logic and computational complexity, and internet routing protocols.


My DBLP entries.

Selected Talks

Kroening Group Seminar, 6 Mar 2014

Marktoberdorf Summer School 2009 Lecture Course: Model Checking Higher-Order Computation. Part 1, Part 2

Research Group Webpage

Current Projects

Centre for Metacomputation   Algorithmic Game Semantics [final report] Verification of Higher-Order Procedural Programs   Implicit Computational Complexity and Resource-Bounded Computation   Internet Routing Procotols: Convergence and Scalability (see a recent press report in today@Lucent).


HOG   Homer