We introduce two-sided type systems, which are a particular kind of 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 symmetrical notions of well-typing and ill-typing, guaranteeing both that well-typed programs don't go wrong and that ill-typed programs do not 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.

翻译：我们引入了双侧类型系统，这是一种特殊的用于类型化公式的相继式演算。双侧类型系统允许对复合程序表达式的类型化进行假设推理，并支持对类型化公式的驳斥。通过纳入全值类型，这些类型系统支持良类型化与不良类型化的对称概念，既保证了良类型程序不会出错，又保证了类型错误程序不会求值——即不会归约到值。这使得双侧类型系统适用于高阶程序验证中的不正确性推理，我们通过在一个包含构造子和模式匹配的语言中应用于精确数据流类型化来加以说明。最后，我们研究了系统中元层次否定的内化，将其作为类型上的互补算子。这激发了类型化判断的另一种语义，该语义保证了类型错误程序不会求值，但良类型程序仍可能出错。