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.
Fields of Study & Subjects
Logic
programming
and type systems
Reasoning
and Knowledge
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Publisher
- Association for Computing Machinery (ACM)
- Volume
- 10
- Issue
- POPL
- Pages
- 2380–2408
- Publication date
- 8 January 2026
- Language
- EN