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.

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