一句话：提出基于上下文类型论的局部上下文类型推断，为 System F 的 LTI 给出首个机械化形式化与算法设计。
类型推断是编程语言的关键技术，但在 System F 等丰富类型系统中，完整全局推断往往不可判定。Pierce 和 Turner 提出的局部类型推断（LTI）依赖应用局部信息，虽被广泛采用，却存在理论不完善、规格复杂且限制过多的问题。本文提出 Local Contextual Type Inference，以 contextual typing 形式化方法重新设计 LTI。作者定义 Contextual System F（F_c），支持隐式与一等多态，给出声明式类型系统，证明可靠性、完备性与可判定性，并引入 matching subtyping 连接声明式与算法推断。该工作是 LTI 的首个机械化处理，去除若干实际限制，展示 contextual typing 在设计稳健、可扩展且易实现类型推断算法方面的能力。
Type inference is essential for programming languages, yet complete and global inference quickly becomes undecidable in the presence of rich type systems like System F. Pierce and Turner proposed local type inference (LTI) as a scalable, partially annotated alternative by relying on information local to applications. While LTI has been widely adopted in practice, there are significant gaps between theory and practice, with its theory being underdeveloped and specifications for LTI being complex and restrictive. We propose Local Contextual Type Inference , a principled redesign of LTI grounded in contextual typing—a recent formalism which captures type information flow. We present Contextual System F ( F c ), a variant of System F with implicit and first-class polymorphism. We formalize F c using a declarative type system, prove soundness, completeness, and decidability, and introduce matching subtyping as a bridge between declarative and algorithmic inference. This work offers the first mechanized treatment of LTI, while at the same time removing important practical restrictions and also demonstrating the power of contextual typing in designing robust, extensible and simple to implement type inference algorithms.
@article{XueCJO26,
title = {Local Contextual Type Inference},
author = {Xu Xue and Chen Cui and Shengyi Jiang and Bruno C. d. S. Oliveira},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776653}
}