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.

翻译：我们引入了一种新的双边类型系统，用于验证具有原子和模式匹配的函数式程序的正确性与不正确性。本工作的一个关键思想是，类型应覆盖正规形式集合而非值集合，这使我们能够在类型上定义一个补运算符，作为类型公式的否定。我们证明，该补运算符允许我们在系统内推导出广泛的证伪原则，包括共蕴含的类型论类比，并利用这些原则认证若干类Erlang程序会出错。通过子类型对补运算符进行表达性公理化被证明是可判定的，且整个类型系统不仅被证明是可靠的，而且对正规形式是完备的。