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.

翻译：常见的函数式语言鼓励使用尾递归函数，而非那些消耗栈空间且可能无法扩展至大规模输入的通用递归函数。这种区分有时要求以尾递归风格编写函数，这可能比自然的非尾递归定义更为复杂且更慢。本文描述了我们在 OCaml 编译器中实现的*尾模构造函数*（TMC）变换，这是一种优化技术，为更广泛的函数类别——*模构造函数*的尾递归函数——提供了栈效率，其中特别包括 `List.map` 的自然定义以及许多类似的递归数据构造函数。我们在一个简化的设定中——一种小型无类型演算——证明了该程序变换的正确性，该设定捕捉了 OCaml 实现的关键特征。我们的证明在 Coq 证明助手中机械化完成，使用了 Iris 基础逻辑。本工作的一个独立贡献是对 Simuliris 方法的扩展，以定义支持不同调用约定的模拟关系。据我们所知，这是首次使用 Simuliris 来证明编译器变换的正确性。