Publications

Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing

We study the foundations of variational inference, which frames posterior inference as an optimisation problem, for probabilistic programming. The dominant approach for optimisation in practice is stochastic gradient descent. In particular, a variant using the so-called reparameterisation gradient estimator exhibits fast convergence in a traditional statistics setting. Unfortunately, discontinuities, which are readily expressible in programming languages, can compromise the correctness of this approach. We consider a simple …
Basim Khajwal, C.-H. Luke Ong, Dominik Wagner 32th European Symposium on Programming (ESOP)
PDF Slides

Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere

We study the differential properties of higher-order statistical probabilistic programs with recursion and conditioning. Our starting point is an open problem posed by Hongseok Yang: what class of statistical probabilistic programs have densities that are differentiable almost everywhere? Our main result is that almost surely terminating SPCF programs, generated from a set of primitive functions satisfying mild closure properties, have weight and value functions that are almost everywhere differentiable.
Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner 30th European Symposium on Programming (ESOP)
PDF Slides Video

Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses

We present initial limit Datalog, a new extensible class of constrained Horn clauses for which the satisfiability problem is decidable. The class may be viewed as a generalisation to higher-order logic (with a simple restriction on types) of the first-order language limit DatalogZ (a fragment of Datalog modulo linear integer arithmetic), but can be instantiated with any suitable background theory.
Toby Cathcart Burn, C.-H. Luke Ong, Steven Ramsay, Dominik Wagner 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PDF

HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories

We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC)—a system of higher-order logic modulo theories generalising (1st-order) constrained Horn clauses—and prove its soundness and refutational completeness w.r.t. both standard and Henkin semantics. As corollaries, HoCHC shares desirable properties (such as semi-decidability and a canonical model property) and deciable fragments with its 1st-order counterpart.
C.-H. Luke Ong, Dominik Wagner 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PDF Slides

Talks

Recent & Upcoming

On the Reparameterisation Gradient for Non-Differentiable but Continuous Models

The Eighth International Workshop on Languages for Inference (LAFI) @ POPL 2023
PDF Poster Slides Video

A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent

Logic of Probabilistic Programming
Slides Video

A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent

The Seventh International Workshop on Languages for Inference (LAFI) @ POPL 2022
Slides

A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent

Differentiable Programming @ NeurIPS 2021
Poster

Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere

30th European Symposium on Programming (ESOP 2021)
Slides Video

HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories

6th Workshop on Horn Clauses for Verification and Synthesis (HCVS)
Slides

Theses

Resolution for Higher−Order Constrained Horn Clauses

Master’s Thesis University of Oxford

Design and Implementation of a CDCL(LA) Calculus

Bachelor’s Thesis Saarland University

Teaching

Graduate Teaching and Research Scholar (Oriel College, Oxford):

Teaching Assistant (University of Oxford):

Teaching Assistant (Saarland University):

  • Fundamentals of Algorithms and Data Structures (winter semester 2016 / 17)
  • Mentor of Mathematical Preparatory Course (Sep / Oct 2016 / 17)

Contact