Publication and News
- January '26 — Domain-theoretic Semantics for Functional Logic Programming published @ POPL
- January '26 — Serving on the POPL Program Committee.
- October '24 — Tom Divers joins as a PhD student.
- January '23 — Higher-Order MSL Horn Constraints published @ POPL
- June '22 — CycleQ: an efficient basis for cyclic equational reasoning published @ PLDI
- January '21 — Intensional datatype refinement: with application to scalable verification of pattern-match safety published @ POPL
We rationally reconstruct a core calculus for FLP that is based on call-by-push-value and algebraic effects.
We show how to execute its programs through an abstract machine that implements narrowing.
Finally, we present a domain-theoretic semantics based on the lower powerdomain, which we prove to be sound, adequate, and fully abstract with respect to the machine.
This leads to an exploration of the limitations of domain theory in modelling FLP.
In this paper, we extend a decidable fragment of a first-order Horn clauses based on automata to a higher-order setting. As an application of this work, we develop an approach to verified socket programming.
We develop a cyclic proof system for automatically reasoning about the equational properties of functional programs that manipulate algebraic datatypes.
The system employs a novel proof inference rule for mitigating equational and inductive reasoning in the context of cyclic proofs as well as an optimised proof search strategy.
We propose a refinement type system aiming to pattern-match safety of a functional program; that is, the absence of patterning matching errors at runtime.
Using a novel restriction on the form of refinements, we develop a sound and complete inference algorithm with a runtime complexity that is, in the worst-case, is linear in the size of the program.