Hugo Paquet
hugo.paquet @ cs.ox.ac.uk
I am a postdoc with Sam Staton working on the theory of probabilistic programming. I am interested in using methods from operational and denotational semantics to improve Bayesian inference.
More broadly I am interested in areas of semantics for programming languages and logics, including game semantics, categorical models, linear logic and models for concurrency, and what happens to all of these in presence of probability.
Until May 2020 I was a postdoc with Luke Ong, and before that (2015-2019) I was a PhD student with Glynn Winskel in the Computer Lab at the University of Cambridge.
Thesis
My thesis is about a theory of games for semantics known as concurrent games, based on event structures.
The main contribution is a cartesian closed bicategory of probabilistic strategies, which gives a semantics for languages with continuous distributions. The manuscript is available here.
Publications and Preprints
- Bayesian strategies: probabilistic programs as generalised graphical models. ESOP 2021. (PDF)
- Densities of almost-surely terminating probabilistic programs are differentiable almost everywhere, with Carol Mak, Luke Ong, and Dominik Wagner. ESOP 2021. (arXiv preprint)
- Probabilistic Programming Inference via Intensional Semantics, with
Simon Castellan. ESOP 2019. (PDF)
- Fully Abstract Models of the Probabilistic Lambda-Calculus, with
Pierre Clairambault. CSL 2018. (PDF)
- Continuous Probability Distributions in Concurrent Games, with
Glynn Winskel. MFPS 2018. (PDF)
- The Concurrent Game Semantics of Probabilistic PCF, with
Simon Castellan,
Pierre Clairambault, and
Glynn Winskel. LICS 2018. (PDF)
- Verification of Multi-Agent Systems via SDD-based Model Checking (Extended Abstract), with
Alessio Lomuscio. AAMAS 2015. (PDF)
Teaching
In Hilary Term 2021 I am lecturing Lambda-calculus and types.
In Cambridge I regularly taught students in various courses including Logic and Proof (sheet1, sheet2, sheet3), Discrete Mathematics (sheet1, sheet2), Semantics, Denotational Semantics, and Hoare Logic and Model Checking.