Ill-Typed Programs Don't Evaluate
Ill-Typed Programs Don't Evaluate
复制标题
类型错误的程序不进行评估
DOI：
10.1145/3632909
复制
发表时间：
2024
影响因子：
--
通讯作者：
Ramsay S
中科院分区：
文献类型：
--
作者：
Ramsay S
我们引入了双边类型系统，它是用于键入公式的顺序演算。双面类型系统允许对复合程序表达式的类型进行假设推理，并对类型公式进行反驳。通过合并所有值的类型，这些类型系统支持更精确的良好类型和不良类型概念，既保证良好类型的程序不会出错，又保证不良类型的程序不会求值——也就是说，不会到达一个值。这使得双面类型系统适合于高阶程序验证中的错误推理，我们通过一个使用构造函数和模式匹配的语言中的精确数据流类型的应用程序来说明这一点。最后，我们研究了元级否定在系统中的内部化，作为类型的补运算符。这激发了类型判断的另一种语义，它保证了类型不良的程序不会求值，但类型良好的程序可能会出错。
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.