Publications
- POPL 23 — Higher-Order MSL Horn Constraints
- PLDI 22 — CycleQ: an efficient basis for cyclic equational reasoning
- POPL 21 — Intensional datatype refinement: with application to scalable verification of pattern-match safety
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.