一句话：提出双侧类型系统，可反驳类型公式，从而保证良类型程序不出错、非良类型程序不会求值。
该文提出双侧类型系统，作为类型公式的相继式演算。它允许对复合程序表达式的类型作假设推理，并能反驳类型公式；通过引入“所有值”的类型，系统给出更精细的良类型与非良类型概念。核心保证是：良类型程序不会出错，而非良类型程序不会求值到值。作者将其用于高阶程序验证中的不正确性推理，并在带构造子和模式匹配的语言中实现精确数据流类型标注。最后，文章把元层否定内化为类型上的补算子，并给出替代类型判定语义：它保证非良类型程序不求值，但良类型程序仍可能出错。
We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By incorporating a type of all values, these type systems support more refined notions of well-typing and ill-typing, guaranteeing both that well-typed programs don’t go wrong and that ill-typed programs don’t evaluate - that is, reach a value. This makes two-sided type systems suitable for incorrectness reasoning in higher-order program verification, which we illustrate through an application to precise data-flow typing in a language with constructors and pattern matching. Finally, we investigate the internalisation of the meta-level negation in the system as a complement operator on types. This motivates an alternative semantics for the typing judgement, which guarantees that ill-typed programs don’t evaluate, but in which well-typed programs may yet go wrong.