一句话：提出以正规形集合为类型语义、带补运算的双侧类型系统，可同时验证函数式程序的正确性与错误性。
论文研究如何对带原子和模式匹配的函数式程序进行错误性类型化，即静态证明程序会“出错”。其核心思想是让类型刻画正规形（normal form）集合而非值集合，从而在类型上定义补算子，并使其在类型公式中充当否定。借助该补算子，系统可导出多种反驳原则，包括类型论中 co-implication 的对应物，并用它们证明若干类 Erlang 风格程序会走向错误。作者给出通过子类型表达的补算子公理化，证明该子类型关系可判定，并证明整个类型系统对正规形既可靠又完备。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2510-13725,
title = {A Complementary Approach to Incorrectness Typing},
author = {Celia Mengyue Li and Sophie Pull and Steven Ramsay},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776724}
}