48 citations · 174 across the 34 of their papers we have counts for
13 papers · 1 filter
Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses
Toby Cathcart Burn, Luke Ong, Steven Ramsay +1
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…
The Difference Lambda-Calculus: A Language for Difference Categories
Mario Alvarez-Picallo, C. -H. Luke Ong
Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of "infinitesimal" arrows satisfying an analogue of the Ko…
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
Christopher H. Broadbent, Arnaud Carayol, C. -H. Luke Ong +1
This paper studies the logical properties of a very general class of infinite ranked trees, namely those generated by higher-order recursion schemes. We consider, for both monadic…
The Extended Theory of Trees and Algebraic (Co)datatypes
Fabian Zaiser, C. -H. Luke Ong
The first-order theory of finite and infinite trees has been studied since the eighties, especially by the logic programming community. Following Djelloul, Dao and Frühwirth, we co…
Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
Carol Mak, C. -H. Luke Ong, Hugo Paquet +1
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 Yan…
Polynomial Probabilistic Invariants and the Optional Stopping Theorem
Anne Schreuder, C. -H. Luke Ong
In this paper we present methods for the synthesis of polynomial invariants for probabilistic transition systems. Our approach is based on martingale theory. We construct invariant…
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories
C. -H. Luke Ong, Dominik Wagner
We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC) - a system of higher-order logic modulo theories - and prove its soundness and refutat…
Change Actions: Models of Generalised Differentiation
Mario Alvarez-Picallo, C. -H. Luke Ong
Cai et al. have recently proposed change structures as a semantic framework for incremental computation. We generalise change structures to arbitrary cartesian categories and propo…
A Type System for proving Depth Boundedness in the pi-calculus
Emanuele D'Osualdo, Luke Ong
The depth-bounded fragment of the pi-calculus is an expressive class of systems enjoying decidability of some important verification problems. Unfortunately membership of the fragm…
Detecting Redundant CSS Rules in HTML5 Applications: A Tree-Rewriting Approach
Matthew Hague, Anthony Widjaja Lin, Luke Ong
HTML5 applications normally have a large set of CSS (Cascading Style Sheets) rules for data display. Each CSS rule consists of a node selector (given in an XPath-like query languag…
Decidable Models of Recursive Asynchronous Concurrency
Jonathan Kochems, C. -H. Luke Ong
Asynchronously communicating pushdown systems (ACPS) that satisfy the empty-stack constraint (a pushdown process may receive only when its stack is empty) are a popular decidable m…
Safety verification of asynchronous pushdown systems with shaped stacks
Jonathan Kochems, C-H Luke Ong
In this paper, we study the program-point reachability problem of concurrent pushdown systems that communicate via unbounded and unordered message buffers. Our goal is to relax the…
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
Naoki Kobayashi, C. -H. Luke Ong
Ong has shown that the modal mu-calculus model checking problem (equivalently, the alternating parity tree automaton (APT) acceptance problem) of possibly-infinite ranked trees gen…