一句话：提出基于 row 多态与子类型的异常追踪类型系统，保持 ML 向后兼容，并在 Rocq 中用关系分离逻辑机械化验证。
本文针对 ML 风格语言中异常缺乏强静态追踪、而既有异常追踪方案又破坏向后兼容的问题，提出一种基于 row 多态与子类型的类型系统。该系统允许不带异常追踪的既有代码继续工作，并可优雅地泛化以支持异常追踪，同时覆盖可扩展变体类型、局部异常与并发等现实特性。为刻画类型系统的安全性与抽象保证（尤其是局部异常对数据抽象的作用），作者提出一种用于异常的新型关系分离逻辑，并以二元逻辑关系表述上述性质，这本身也是独立贡献。评估涵盖来自 OCaml 标准库、Jane Street 的 OCaml 库以及 Filinski 博士论文中的多个挑战性例子，所有结果均在 Rocq 证明助手中基于 Iris 机械化验证。
We introduce a type system that provides strong types for exception tracking in ML-style languages. Our type system employs a rich notion of row polymorphism and subtyping to ensure backwards compatibility, making sure that code without exception tracking continues to work and can be generalized gracefully to support exception tracking. We study the safety and abstraction guarantees of our type system, in particular the role of local exceptions for data abstraction. We formulate these claims using binary logical relations in a novel relational separation logic for exceptions, an independent contribution of this paper. We support a realistic subset of features from ML-style languages, such as extensible variant types, local exceptions, and concurrency. We exercise our type system and logic on a number of challenging examples taken from the OCaml standard library, from one of Jane Street's OCaml libraries, and from Filinski's PhD thesis. All our results are mechanized in the Rocq prover using Iris.
@article{CollemVK26,
title = {Backwards-Compatible Row-Based Exceptions in ML},
author = {Simcha van Collem and Paulo Emílio de Vilhena and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808303}
}