Embedded Files
Our Vision
We make foundational software more reliable and scalable.
We focus on fundamental programs & computations across diverse areas (e.g., machine learning, scientific computing).
We prove their correctness, improve their efficiency, and understand their fundamental limits.
Our Directions
We analyze existing, practically-used software from theoretical perspectives.
We design and develop new, practical software with theoretical guarantees.
We characterize the fundamental limits of all such software.
Our Tools
Programming Languages (program analysis, semantics, language design, proof assistants, compilers)
Numerical Computations (floating-point numbers, computable reals)
Mathematics (real analysis, probability theory)
Function Evaluation
Problem
How can we compute common math functions (e.g., exp) correctly and efficiently?
Relevant Software: GNU C Library, LLVM C Library, CORE-MATH, ...
Our Work
Random Variate Generation
Problem
How can we sample from common probability distributions (e.g., Normal) correctly and efficiently?
Relevant Software: GNU Scientific Library, SciPy, PyTorch, ...
Our Work
Differentiation
Problem
How can we compute derivatives of programs correctly and efficiently?
Relevant Software: PyTorch, TensorFlow, JAX, ...
Our Work
Integration / Probabilistic Inference
Problem
How can we compute integrals of programs correctly and efficiently?
How can we sample from posterior distributions correctly and efficiently?
Relevant Software: Pyro, Stan, Gen, ...
Our Work
(POPL'26) Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
(PLDI'25) Semantics of Integrating and Differentiating Singularities
(POPL'20) Towards Verified Stochastic Variational Inference for Probabilistic Programs
(AAAI'20) Differentiable Algorithm for Marginalising Changepoints
Function Approximation
Problem
Which functions can neural networks approximate accurately?
Relevant Software: PyTorch, TensorFlow, Flax, ...
Our Work
Google Sites
Report abuse