48 citations · 174 across the 34 of their papers we have counts for
15 papers · 1 filter
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing
Basim Khajwal, C. -H. Luke Ong, Dominik Wagner
We study the foundations of variational inference, which frames posterior inference as an optimisation problem, for probabilistic programming. The dominant approach for optimisatio…
CycleQ: An Efficient Basis for Cyclic Equational Reasoning
Eddie Jones, C-. H. Luke Ong, Steven Ramsay
We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proof and…
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
Andrew Kenyon-Roberts, Luke Ong
We introduce a method for proving almost sure termination in the context of lambda calculus with continuous random sampling and explicit recursion, based on ranking supermartingale…
Verifying Liveness Properties of ML Programs
M. M. Lester, R. P. Neatherway, C. -H. L. Ong +1
Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algor…
A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
Carol Mak, Luke Ong
Building on the observation that reverse-mode automatic differentiation (AD) -- a generalisation of backpropagation -- can naturally be expressed as pullbacks of differential 1-for…
Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog
Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones +1
Incremental computation has recently been studied using the concepts of change structures and derivatives of programs, where the derivative of a function allows updating the output…
Defunctionalization of Higher-Order Constrained Horn Clauses
Long Pham, Steven J. Ramsay, C. -H. Luke Ong
Building on the successes of satisfiability modulo theories (SMT), Bjørner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic progr…
Higher-Order Constrained Horn Clauses and Refinement Types
Toby Cathcart Burn, C. -H. Luke Ong, Steven J. Ramsay
Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision proble…
On Hierarchical Communication Topologies in the pi-calculus
Emanuele D'Osualdo, C. -H. Luke Ong
This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if…
Normalisation by Traversals
C. -H. Luke Ong
We present a novel method of computing the beta-normal eta-long form of a simply-typed lambda-term by constructing traversals over a variant abstract syntax tree of the term. In co…
Fragments of ML Decidable by Nested Data Class Memory Automata
Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski +1
The call-by-value language RML may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct in the sense of Reynolds.…
Innocent Strategies are Sheaves over Plays---Deterministic, Non-deterministic and Probabilistic Innocence
Takeshi Tsukada, C. -H. Luke Ong
Although the HO/N games are fully abstract for PCF, the traditional notion of innocence (which underpins these games) is not satisfactory for such language features as non-determin…
Automatic Verification of Erlang-Style Concurrency
Emanuele D'Osualdo, Jonathan Kochems, C. -H. Luke Ong
This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce Lambda-Actor, a p…
Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming
Martin Lester, Luke Ong, Max Schaefer
Web applications written in JavaScript are regularly used for dealing with sensitive or personal data. Consequently, reasoning about their security properties has become an importa…
The Safe Lambda Calculus
William Blum, C. -H. Luke Ong
Safety is a syntactic condition of higher-order grammars that constrains occurrences of variables in the production rules according to their type-theoretic order. In this paper, we…