On the Theory of Structural Subtyping
我们证明了非递归类型的结构子类型的一阶理论是可判定的。设$Σ$是一种由函数符号（表示类型构造函数）组成的语言，$C$是关系语言$L$中包含二元关系$\leq$的可判定结构。$C$表示基本类型; $\leq$表示子类型排序。我们引入了$Σ$-$C$的项幂的概念，它概括了结构子类型中出现的结构。$C$的$Σ$ -项-幂的域是$C$的元素集合上的$Σ$ -项的集合。我们证明了$C$的一阶理论的可判定性意味着$C$的$Σ$ -项-幂的一阶理论的可判定性。我们的决策过程中使用的量词消去的项代数和Feferman-Vaught定理。我们的结果暗示了非递归类型的结构子类型的一阶理论的可判定性。
2004-08-05 cs.LO cs.PL cs.SE
On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping
会话类型是保证并发程序没有基本通信错误的行为类型。最近的工作表明，异步会话子类型是不可判定的。然而，由于会话类型在主流程序设计语言中变得流行，其中异步通信是规范而不是例外，因此检测重要的可判定子类型关系至关重要。以前的工作考虑了限制性极强的片段，其中限制被施加到通信缓冲区的大小（最多1）或表达多个选择的可能性（不允许他们完全在一个比较类型）。在这项工作中，第一次，我们展示了一个片段，不施加任何限制，通信缓冲区，并允许两个比较的类型，包括多个选择的输入或输出，从而产生一个片段，这是更重要的适用性的观点。一般来说，我们通过考虑子类型的几个片段来研究可判定性和不可判定性之间的边界。值得注意的是，我们表明，子类型仍然是不可判定的，即使限制不使用输出协方差和输入逆变。
2018-02-12 cs.PL
Subtyping Context-Free Session Types
本文针对上下文无关会话类型子类型化不可判定问题，提出基于$\mathcal{XYZW}$-模拟的子类型化方法及可靠算法，并在编译器环境中验证了其实用性。
2023-09-20 cs.PL
Towards Algebraic Subtyping for Extensible Records
针对MLsub仅支持不可扩展的显式类型化记录的问题，研究通过向Simple-sub推断算法的类型语言加入行变量、扩展约束求解方法，实现了可扩展记录支持且保留类型推断可判定性。
2024-07-09 cs.PL
Regular Expression Subtyping for XML Query and Update Languages
XML数据库查询语言（如XQuery）使用具有结构子类型的正则表达式类型。子类型系统通常有两种表现形式，它们应该是等价的：一种是声明性版本，其中包含规则可以在任何地方使用，另一种是算法版本，其中包含规则的使用受到限制，以便使类型检查语法导向和可判定。然而，XQuery标准类型系统通过对迭代构造使用不精确的类型规则并仅定义算法类型检查来规避这个问题，另一个现存的提议为迭代构造提供了更精确的类型，但忽略了子类型。在本文中，我们考虑一个核心的类XQuery语言的包容规则，并证明算法的类型检查的完整性，这是简单的XQuery正确的，但需要一些照顾更精确的迭代类型的纪律存在。我们将这一结果扩展到我们在早期工作中介绍的XML更新语言。
2008-01-04 cs.DB cs.PL
BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
BinSub 通过代数子类型化框架实现简单、精确且高效的二进制类型推断，在保持与先前工作相似精度的同时将 1568 个函数的平均运行时间提升了 63 倍。
2024-09-03 cs.PL
Typechecking without Minimum Types: Finite Bases and Backward Checking for $F_{<:}^{\top}$
Capital Normal University（首都师范大学）；Kean University（基恩大学）
针对缺乏最小类型的 $F_{<:}^{\ op}$，提出有限基与反向检查方法，证明其类型检查可判定，且两种检查过程为等价的完整 Rocq 函数，符号实现具四次方最坏复杂度。
2026-10-14 cs.PL
Polarized Subtyping
按推值调用中类型的极化自然导致归纳定义的可观察值（按正类型分类）和共归纳定义的计算（按负类型分类）的分离，伴随模态在它们之间进行调解。以这种分离为出发点，我们开发了一个语义特征的类型与步骤索引捕捉观察深度的递归计算。这种语义为推值调用的等递归变体（包括变体和惰性记录）提供了丰富的子类型规则集。我们进一步提出了一个双向的语法类型化系统的值和计算，优雅和务实地规避困难的类型推断的宽度和深度的子类型的变体和懒惰的记录。我们展示了我们的系统的灵活性，系统地派生相关系统的子类型（a）isorecursive类型，（b）调用的名称，和（c）调用的值，所有使用的结构，而不是名义上的解释类型。
2022-01-26 cs.LO cs.PL
Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas
在最近的工作中，我们已经展示了如何通过将程序抽象编译成Horn公式f来为面向对象语言定义非常精确的类型系统。那么类型推断就等于解决了一个特定的目标。f的共归纳（也就是最大的）Herbrand模型。以这种方式定义的类型系统是理想化的，因为在最有趣的实例化中，共同归纳的Herbrand论域和目标导子的项都不能被直接表示。然而，声音和相当有表现力的近似可以通过只考虑正则项和导数来实现。在这样做的时候，引入一个适当的子类型关系来形式化类型之间近似的概念是至关重要的。本文研究了建立在联合和对象类型构造函数上的共归纳项的子类型关系。我们定义了一个解释的类型作为一组值引起的一个相当直观的关系的成员资格的值类型，并证明了子类型的定义是健全的w.r.t.类型解释之间的子集包含。可靠性的证明使我们能够简化压缩派生的概念，并发现先前给出的子类型定义并没有涵盖空类型的所有可能表示。
2010-06-08 cs.LO cs.PL
Polymorphic Type Inference for Dynamic Languages
本文提出一种结合一阶多态性、交集/并集类型及子类型的类型系统，并设计可靠且可终止的类型重构算法，使未标注函数获得多态类型以表达重载行为，适用于动态语言类型化。
2023-11-17 cs.PL
First-Class Refinement Types for Scala
EPFL（洛桑联邦理工学院）
本文提出在 Scala 3 中实现第一类细化类型，使细化类型能参与子类型、推断和模式匹配，提升类型安全性和实用性。
2026-09-25 cs.PL
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
本文提出利用捕获数据流的子类型约束来解释类型错误，将错误展示为相关程序位置的数据流序列，并可与 Hindley-Milner 推断集成，用户研究表明基于流的错误消息具有实际需求。
2024-02-20 cs.HC cs.PL
Type Inference for Static Compilation of JavaScript (Extended Version)
我们提出了一个类型系统和推理算法的丰富子集的JavaScript配备对象，结构子类型，原型继承，和一流的方法。该类型系统支持抽象和递归对象，并且具有足够的表达能力，可以容纳几个标准基准测试，而只需要一些较小的变通方法。由类型强制执行的不变量使提前编译器能够执行动态语言的静态编译器通常无法达到的优化。与以前的推理技术原型继承，我们的算法使用了一个组合的下限和上限传播推断类型和发现类型错误的所有代码，包括未调用的功能。推理表示在一个简单的约束语言，旨在利用现成的固定点求解器。我们证明了类型系统和推理算法的合理性。实验评估表明，推理是强大的，处理上述基准没有手动类型注释，并推断类型实现有效的静态编译。
2016-10-18 cs.PL
Type Inference for Bimorphic Recursion
本文提出了双态递归，这是一种受限制的多态递归，使得函数定义体中的每个递归调用具有相同的类型。双态递归允许我们为递归定义的函数分配两种不同的类型：一种是递归调用，另一种是定义之外的调用。本文中的双态递归是可以嵌套的。本文证明了双态递归具有主类型和可判定的类型推断。因此，双态递归给我们提供了灵活的递归类型和可判定的类型推断。本文还表明，它的类型成为不可判定的，因为嵌套的递归时，从双态递归删除的实例化属性。
2011-06-07 cs.LO cs.PL
Practical Refinement Session Type Inference (Extended Version)
University of Edinburgh（爱丁堡大学）；Boston University（波士顿大学）
本文提出了一种带算术细化的会话类型系统类型推断算法，并通过优化使其在实际应用中可行。
2026-02-06 cs.PL
Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
University of Wrocław（弗罗茨瓦夫大学）
本文提出一种针对带子类型和高阶多态的类型-效果系统的效果推断算法，通过将约束转为命题逻辑延迟求解，证明其健全性与完备性，并在现实语言中实现。
2025-10-23 cs.PL
On Hierarchical Communication Topologies in the pi-calculus
本文研究π-项的通信拓扑所满足的形状不变量，以及这些不变量的自动推理。π-项P是层次的，如果存在有限森林T，使得从P可达的每个项的通信拓扑满足T形不变量。我们设计了一个静态分析，通过一个新的类型系统，享有决策推理证明一个术语层次。类型系统的可靠性证明采用了π演算反应的非标准观点。层次项的可覆盖性问题是可判定的。这是证明了每一个层次的长期是深度有界的，在文献中已知的不可判定的属性。因此，我们得到一个有表现力的静态片段的π演算可判定的安全验证问题。
2016-04-19 cs.LO cs.PL
Gradual Liquid Type Inference
液态类型提供了一种可判定的细化推理机制，它很方便，但有两个主要问题：（1）推理是全局的，需要顶级注释，这使得它不适合模块化代码组件的推理，并禁止其适用于库代码，以及（2）推理失败导致模糊的错误消息。这些困难严重阻碍了现有代码的迁移以使用改进。本文表明，逐步液体类型推断-液体推理和逐步细化类型的新组合-解决这两个问题。支持乐观解释的不精确谓词的渐进细化类型可以在参数位置中使用以约束流动推理，使得全局推理过程e有效地推断可用于库组件的模块化规范。双重地，当逐渐改进作为推理的结果出现时，它们表示静态改进的使用不一致。因为液体细化是从一个nite集合的谓词，在逐渐液体类型推断，我们可以枚举每个不精确的细化的安全具体化，即静态细化，证明为什么一个程序是逐渐良好的类型。此枚举对于静态液体类型错误的解释非常有用，因为安全具体化显示了导致静态类型错误的所有潜在不一致性。我们发展了渐进式液态类型推断理论，并在液态Haskell语言环境下对其语用进行了探讨。
2019-10-30 cs.PL
Inferring Region Types via an Abstract Notion of Environment Transformation
基于区域的类型系统是各种程序分析的有力工具。我们引入了一个新的推理算法的区域类型的基础上的抽象概念的环境转换。它只分析一个方法的代码一次，即使程序中有不同区域类型的方法的多次调用。这种抽象转换的元素本质上是相等和子类型的约束，它们捕获程序的流信息。特别是，我们的工作与访问图的抽象转换的定义，以保证终止的推理算法，因为它们提供了一个有限的表示字段访问路径。
2022-09-07 cs.LO cs.PL
Polymorphic Type Inference for Machine Code
对于许多编译语言，源代码级别的类型在编译过程的早期就被擦除。因此，进一步的编译器遍数可能会将类型安全的源代码转换为类型不安全的机器码。原始源代码中的类型不安全习惯用法和类型不安全优化意味着剥离的二进制文件中的类型信息基本上不存在。通过在剥离的机器码上执行类型推断来恢复高级类型的问题被称为类型重构，并且提供了支持逆向工程和反编译的有用能力。在本文中，我们激励和开发一个新的类型系统和算法的机器代码类型推断。这个类型系统的特征是通过调查广泛的常见源代码和机器代码习惯用法，建立一个类型重建的挑战性案例目录来开发的。我们发现，这些习惯用法对类型系统提出了一组复杂的要求，并引入了递归约束多态类型等特性。我们所识别的许多特性通常只在高级函数式语言所使用的表达性强且功能强大的类型系统中才能看到。使用这些类型系统的功能作为指导方针，我们已经开发了Retypd：一个新的静态类型推理算法的机器码，支持递归类型，多态性和子类型。Retypd产生比现有算法更准确的推断类型，同时还支持新功能，例如以98%的召回率重建指针常量注释。Retypd可以在比现有技术更弱的程序表示上操作，从而消除了对可能无法计算的高质量指向信息的需求。
2016-03-18 cs.LO cs.PL
A tier-based typed programming language characterizing Feasible Functionals
本文提出一种基于分层类型系统的命令式编程语言，可判定地刻画基本可行泛函类 BFF$_2$，其类型推断复杂度为程序规模的立方级，连接高阶复杂度与编程理论。
2022-02-23 cs.LO cs.PL
Transformer Models for Type Inference in the Simply Typed Lambda Calculus: A Case Study in Deep Learning for Code
IHES（高等科学研究所）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；IBM Research（IBM研究院）
本文提出以项与类型关系为核心的基准，研究 transformer 在简单类型 lambda 演算类型推断中的预热与优化器选择，发现 Adafactor 较 Adam 和 RAdam 收敛更快。
2023-03-15 cs.AI cs.LG cs.LO
