research
∙
01/09/2023
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing
We study the foundations of variational inference, which frames posterio...
share
research
∙
11/24/2021
CycleQ: An Efficient Basis for Cyclic Equational Reasoning
We propose a new cyclic proof system for automated, equational reasoning...
research
∙
11/30/2020
The Difference Lambda-Calculus: A Language for Difference Categories
Cartesian difference categories are a recent generalisation of Cartesian...
research
∙
10/13/2020
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
This paper studies the logical properties of a very general class of inf...
research
∙
10/13/2020
Collapsible Pushdown Parity Games
This paper studies a large class of two-player perfect-information turn-...
research
∙
05/13/2020
The Extended Theory of Trees and Algebraic (Co)datatypes
The first-order theory of finite and infinite trees has been studied sin...
research
∙
04/08/2020
Densities of almost-surely terminating probabilistic programs are differentiable almost everywhere
We study the differential properties of higher-order statistical probabi...
research
∙
10/25/2019
Polynomial Probabilistic Invariants and the Optional Stopping Theorem
In this paper we present methods for the synthesis of polynomial invaria...
research
∙
02/27/2019
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...
research
∙
02/14/2019
Change Actions: Models of Generalised Differentiation
Cai et al. have recently proposed change structures as a semantic framew...
research
∙
10/08/2018
Defunctionalization of Higher-Order Constrained Horn Clauses
Building on the successes of satisfiability modulo theories (SMT), Bjørn...
research
∙
05/17/2017
