A Complementary Approach to Incorrectness Typing
Abstract
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 types should range over sets of normal forms, rather than sets of values, and this allows us to define a complement operator on types that acts as a negation on typing formulas. We show that the complement allows us to derive a wide range of refutation principles within the system, including the type-theoretic analogue of co-implication, and we use them to certify that a number of Erlang-like programs go wrong. An expressive axiomatisation of the complement operator via subtyping is shown decidable, and the type system as a whole is shown to be not only sound, but also complete for normal forms.
Cite
@article{arxiv.2510.13725,
title = {A Complementary Approach to Incorrectness Typing},
author = {Celia Mengyue Li and Sophie Pull and Steven Ramsay},
journal= {arXiv preprint arXiv:2510.13725},
year = {2026}
}
Comments
The main text of this paper was published at POPL'26. This version of the appendices includes an essential change to the statement of Inversion (and its proof) after a flaw was identified by Tomos Sherlock: the new Inversion theorem only applies when the main subject is a closed term