Statistical probabilistic and differentiable programming, programming languages, verification, semantics of computation, logic and algorithms, security, algorithmic game theory.
My major research contributions are in programming language semantics and applications to the theory and practice of verification.
My research has been broad, ranging across semantics of computation, programming languages, verification, logic and algorithms, and recently, probabilistic and differential programming. A feature of my work is the combination of ideas and methods from semantics and structures, with algorithmic techniques from automated verification. I coinvented and have played a leading role in the development of game semantics and its applications, and higher-order model checking.
The Full Abstraction Problem (Milner 1977, Plotkin 1977, Scott 1969) calls for a denotational model of PCF (a prototypical language) that satisfies a strong goodness-of-fit criterion. Throughout the 1970s to the early 1990s, this was the most significant open problem in the semantics of programming languages, driving key innovations. The problem was finally settled by Hyland and Ong [FPCA 1995, Inf & Comp 2000] and independently by Abramsky et al. Our solution opened up the field of game semantics of programming languages. This work was recognised by the 2017 ACM/IEEE/EATCS Alonzo Church Award for Outstanding Contributions to Logic and Computation.
Hyland-Ong games are the basis of a unifying theory of programming language semantics. We have used game semantics to classify the "space of programming languages" by systematically constructing fully abstract models for a wide spectrum of programming languages, with features ranging across higher-order procedural, nominal [LICS04], nondeterministic [LICS15b], concurrent [ICALP04], probabilistic [LICS15], non-local control; and variously typed [ICALP12, TCS02, TCS03].
The impact of game semantics reaches beyond pure semantic theory to a variety of applications. I have played a leading role in algorithmic game semantics, the application of game semantics to software model checking [TACAS04, CAV09, ICALP11, CAV12, LICS02, ICALP05]. A key result [LICS02] gives the first infinite-state automata-theoretic characterisation of a decidable fragment of the higher-order procedural language Idealised Algol; a complete classification was achieved in [ICALP05]. Game semantics has provided tools for the verification of a wide range of computational systems, such as reactive systems of timed and hybrid automata, higher-order and mobile processes, and the model checking of higher-order programs. There has also been significant influence in other areas such as higher-type complexity theory, static program analysis, type systems, resource-sensitive compilation, and compiler certification.
Model checking is a successful approach to program verification that promises accurate analysis with push-button automation. Since the 1990s, huge strides have been made in the verification of first-order programs by model checking. The field of Higher-order model checking extends model checking to higher order computation. In [LICS06] I showed that the (monadic second-order logic) model checking of infinite trees generated by recursion schemes is decidable (n-EXPTIME complete where n is the order of the scheme). This result was surprising because such trees are extremely expressive; and significant because recursion schemes capture the computational trees of higher-order programs.
With collaborators, I have established further significant results in higher-order model checking:
These algorithmic constructions have yielded successful tool implementations of model checkers of higher-order programs [POPL14, POPL11].
My other more recent research achievements include:
Construction of Soter, the first fully-automatic, infinite-state model checker for Erlang [SAS13]; design of the first reachability algorithm for communicating pushdown systems via unbounded and unordered buffers without the empty stack constraint [CONCUR13]; introduction of a new decidable class of concurrent message-passing systems via a shape constraint on the communication topology [ESOP16].
Development of the first information flow analysis for staged metaprogramming [CSF13]; and a new expressive class of security protocols with an unbounded number of sessions and unrestricted fresh data for which secrecy is decidable [CSF17].
Systematic study of quantitative models relating game semantics, resource calculus, intersection types, and relational models [LICS16, LICS17a]; a new syntactic representation theory (based on the rigid resource calculus) of the generalised species of Fiore et al. [LICS17b]; construction of a unified modelling framework, based on weighted generalised species, where weights are morphisms of a given symmetric monoidal closed category, that induces adequate models of nondeterministic, probabilistic, algebraic and quantum programming languages by an appropriate choice of the weight category [LICS18].
Introduction of higher-order constrained Horn clauses---a refutationally complete and semantically invariant system of higher-order logic modulo theories [POPL18, LICS19]---for verifying higher-order programs; and the first extensible class of decidable constrained Horn clauses over a non-trivial background theory [LICS21a].
Methods of proving almost-sure termination of probabilistic programs [PLDI21, LICS21b]; proof of Yang's conjecture: the density functions of almost surely terminating probabilistic programs are almost everywhere differentiable [ESOP21]; and design of nonparametric Hamiltonian Monte Carlo, the first general purpose inference algorithm that works out-of-the-box for programs in a universal probabilistic programming language [ICML21].