The big picture
My overarching ambition is to develop formalisms which will significantly improve our understanding of complex dynamic systems.
Theoretical computer science has created powerful frameworks to reason about programs and networks, which are extremely complex dynamical systems. My favourite such framework could be called the algebra-coalgebra picture. Specifying and reasoning about systems is done using formal languages which can essentially be seen as algebraic constructs, whilst the modeling of systems can almost always be seen as generalized transition systems, neatly captured by the notion of coalgebra. The connection between algebra and coalgebra is given by the fact that formal specification languages – viz. algebras – are interpreted in generalized transition systems – viz. coalgebras.
The problem with this picture (there is always a problem!), is that coalgebras are very ill-suited to implementing key aspects of what is expected of a dynamical system. They don’t really have a satisfying notion of dynamics for a start (they don’t vary over time, or under the influence of actions), and they do not usually support important concepts like symmetries.
On the other hand mathematics has developed extremely powerful quantitative modeling paradigms such as stochastic processes, which do offer rich and effective methods such as stochastic differential equations, group actions, etc to study the evolution and symmetries of dynamical systems.
My overall vision is to reconcile these two worlds. This means on the one hand extracting formal structures from mathematical models (“reverse semantics”) – in the spirit if my work on structural probability theory (see below); and on the other hand providing more sophisticated semantics to formal languages (“forward semantics”) which allow important notions like evolution and symmetry – in the spirit of my work on probabilistic network programming (see below). The two approaches should hopefully join up with the development of a “natural” syntax and a semantics for probabilistic programming.
Current and recent research
1. Syntax and Semantics for Probabilistic Programming.
I am currently working with Dexter Kozen from Cornell University on the development of a simple imperative language with enough features to express probabilistic programs written in, for example, Anglican or Probabilistic C. The language aims to include conditioning as a primitive operation. Parallel to the development of a syntax and type system, we are developing the mathematical infrastructure to provide the language with both a denotational semantics in terms of Markov kernels, and an operational semantics in terms of sampling. My long-term ambition is to be able to prove the correctness of important algorithms in statistical machine learning, such a Gibbs sampling for example.
2. Structural Probability Theory and Foundations of Bayesian Learning.
With my colleagues Vincent Danos and Ilias Garnier from ENS Paris we have in the last couple of years embarked on an ambitious project aiming to develop a structural approach to probability theory, using ideas from category theory. This is a new and exciting area of research which stems partly from the need to formalise notions of approximation for probabilistic systems (for example, to approximate the stochastic semantics of kappa, a rule-based language for modeling protein interaction networks), but also from the emergence of probabilistic programming as a new programming paradigm. In a series of publications, we have shown how well-known probabilistic constructs, such as the Dirichlet and Poisson processes used in machine learning, are instances of well-known categorical constructs called natural transformation and are entirely determined by their finite components. In another strand of research we have shown in a pair of papers how Bayesian inversion, the mathematical engine room of Bayesian learning, can be re-interpreted as computing the adjoint of a linear operator.
3. Probabilistic network programming.
I am part of Alexandra Silva‘s team working on the foundations of probabilistic network semantics. Amongst our avenues of research are questions about what a good notion of probabilistic Kleene algebras should be, what their semantics would be, and how automata-theoretic constructions translate in the probabilistic case. I also plan to investigate how network symmetries could be used to significantly reduce the size and complexity of probabilistic network verification problems.
4. Coalgebraic Logic.
During my Ph.D. and in subsequent publications I have developed a solution to the long-standing problem in coalgebraic logics of proving completeness for logics with axioms of arbitrary modal depth by generalizing a technique of modal logic called “completeness-via-canonicity” to coalgebraic logics. From 2014 to 2016 I have worked with David Pym who was interested in applying the techniques developed in my Ph.D. thesis to the substructural logic underpinning separation logic (boolean BI) and its modal extensions. We published a coalgebraic completeness result for all distributive substructural logic with a very natural relational semantics. This result is completely modular, and many modal extensions of separation logic can thus also be given a complete semantics, in particular dynamic separation logics. I am currently collaborating with Alexander Kurz on the exciting new topic of positive coalgebraic logics.