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程序的错误行为。通过子类型化对补算子进行的表达性公理化被证明是可判定的，并且整个类型系统不仅被证明是可靠的，而且对于正规形式也是完备的。