一句话：提出模式穿越与模态种类，使 OxCaml 可自动强化模态类型，减少注解并保持无数据竞争。
OxCaml 通过模式（mode）扩展 OCaml 类型系统，以保证并发程序无数据竞争，但模态跟踪常会拒绝明显安全的程序，例如跨线程共享不可变数据。本文提出模式穿越（mode crossing），允许对特定类型的值自动强化模式（如从 nonportable 到 portable），显著减少模态类型注解负担。为支持抽象类型规范，作者进一步引入模态种类（modal kinds），给出其类型论刻画，将其解释为模式格上的单调函数，并扩展到递归与抽象类型。作者在 Iris 之上用 Rocq 验证该系统的可靠性。论文还设计推断过程，将种类检查与包含关系归约为专用格求解器约束，并在 OxCaml 编译器中实现、部署于大型工业代码库，展示其实用性。
OxCaml extends the OCaml type system with support for safe low-level systems programming via modes . For example, OxCaml’s modal portability and contention axes ensure that concurrent OxCaml programs have no data races. In practice, however, modal tracking can reject programs that are obviously safe, such as when the data shared across threads is immutable. To remedy this problem, we introduce mode crossing —the ability to automatically strengthen modes ( e.g. , from nonportable to portable) for values of certain types. Mode crossing significantly reduces the annotation burden associated with modal types. To support mode crossing in the presence of abstract type specifications, we further introduce a new type system feature, modal kinds . We present a type-theoretic account of modal kinds, interpret them as monotone functions on a lattice of modes, and extend this interpretation to recursive and abstract types. We verify soundness of the modal kind system in Rocq on top of Iris. We design an inference procedure that reduces kind checking and subsumption to constraints solved by a dedicated lattice solver. Our design is implemented in the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.
@article{PetersJKSSDE26,
title = {Mode Crossing},
author = {Benjamin Peters and Jules Jacobs and Diana Kalinichenko and Liam Stevenson and Aspen Smith and Derek Dreyer and Richard A. Eisenberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828681}
}