一句话：首个可靠完备判定过程：无表达式类型标注、含不规则递归泛型接口的名义式OO程序可验证；标签监听器和类型一致性实现类型外推。
本文研究名义式面向对象泛型语言中表达式缺少类型标注时的程序验证问题，尤其针对具有不规则递归签名泛型接口，这类语言难以沿用结构化类型的可判定性方案。作者将事件驱动的标签监听器引入约束系统，按需生成程序验证的复杂条件，同时保证终止；并提出类型一致性这一新的声明式程序有效性概念，可在无需类型推断所需复杂类型文法的情况下确保安全性。由于可推断性蕴含类型一致性而反之不成立，算法可不推断缺失类型而直接判定有效性，故称类型外推。作者在 Rocq 中机器化形式化并验证了类型一致性、类型外推与标签监听器，给出首个可靠且完备的判定过程，为超越结构化类型限制的可判定性奠定基础。
We present the first sound and complete decision procedure capable of validating nominal object-oriented programs without type annotations in expressions even in the presence of generic interfaces with irregularlyrecursive signatures. Such interface signatures are exemplary of the challenges an algorithm must overcome in order to scale to the needs of modern major typed object-oriented languages. We do so by incorporating event-driven label-listeners into our constraint system, enabling more complex aspects of program validation to be generated on demand while still ensuring termination. Furthermore, we define type-consistency as a novel declarative notion of program validity that ensures safety without requiring a complex grammar of types to perform inference within. While type-inferability ensures type-consistency, the converse does not necessarily hold. Thus our algorithm decides program validity without inferring the types missing from the program, and so we instead call it a type-outference algorithm. By bypassing type-inference, the proofs involving type-consistency more directly connect the design of and reasoning about constraints to the operational semantics of the language, simplifying much of the design and verification process. We mechanically formalize and verify these concepts and techniques—type-consistency, type-outference, and label-listeners—in Rocq to provide a solid foundation for scaling decidability beyond the limitations of structural types.
@article{paperbot2927,
title = {Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics},
author = {Ross Tate},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763797}
}