3 citations · 10 across the 12 of their papers we have counts for
12 papers
Logical Foundations of Two-Sided Type Theory
Celia Mengyue Li, Steven Ramsay
Two-sided type systems, introduced in POPL'24, are an extension of the traditional notion of type system that allows for stating and deriving typing judgements in which (a) assumpt…
A Complementary Approach to Incorrectness Typing
Celia Mengyue Li, Sophie Pull, Steven Ramsay
We introduce a new two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea in the work is that type…
Ill-Typed Programs Don't Evaluate
Steven Ramsay, Charlie Walpole
We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expr…
Effect Handlers for Programmable Inference
Minh Nguyen, Roly Perera, Meng Wang +1
Inference algorithms for probabilistic programming are complex imperative programs with many moving parts. Efficient inference often requires customising an algorithm to a particul…
Higher-Order MSL Horn Constraints
Jerome Jochems, Eddie Jones, Steven Ramsay
The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in…
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…
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…
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…
Intensional Datatype Refinement
Eddie Jones, Steven Ramsay
The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement t…
Bisimilarity in fresh-register automata
Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos
Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order…
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…