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.
Kroening Group Seminar, 6 Mar 2014
Marktoberdorf Summer School 2009 Lecture Course: Model Checking Higher-Order Computation. Part 1, Part 2
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).