一句话：在 OCaml 编译器中实现 tail modulo cons 变换，并用 Coq/Iris 机器化证明其正确性。
主流函数式语言鼓励尾递归，但 List.map 等自然递归定义会消耗栈空间，改写成尾递归风格往往更复杂也更慢。本文在 OCaml 编译器中实现了 tail modulo cons（TMC）变换，使「模构造子尾递归」的一大类函数也能获得栈效率。为证明该变换的正确性，作者在一个小的无类型演算中刻画 OCaml 实现的关键要点，并在 Coq 的 Iris 基础逻辑中完成机器化验证；作为独立贡献，工作还扩展了 Simuliris 方法，定义支持不同调用约定的模拟关系。据作者所知，这是 Simuliris 首次被用于证明编译器变换的正确性。
Common functional languages incentivize tail-recursive functions, as opposed to general recursive functions that consume stack space and may not scale to large inputs. This distinction occasionally requires writing functions in a tail-recursive style that may be more complex and slower than the natural, non-tail-recursive definition. This work describes our implementation of the tail modulo constructor (TMC) transformation in the OCaml compiler, an optimization that provides stack-efficiency for a larger class of functions — tail-recursive modulo constructors — which includes in particular the natural definition of List.map and many similar recursive data-constructing functions. We prove the correctness of this program transformation in a simplified setting — a small untyped calculus — that captures the salient aspects of the OCaml implementation. Our proof is mechanized in the Coq proof assistant, using the Iris base logic. An independent contribution of our work is an extension of the Simuliris approach to define simulation relations that support different calling conventions. To our knowledge, this is the first use of Simuliris to prove the correctness of a compiler transformation.
@article{paperbot3221,
title = {Tail Modulo Cons, OCaml, and Relational Separation Logic},
author = {Clément Allain and Frédéric Bour and Basile Clément and François Pottier and Gabriel Scherer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704915}
}