Tail Modulo Cons, OCaml, and Relational Separation Logic

This 21-minute conference talk from POPL 2025 presents research on implementing the tail modulo constructor (TMC) transformation in the OCaml compiler. Explore how this optimization enables stack-efficiency for a broader class of functions called "tail-recursive modulo constructors," which includes natural implementations of List.map and similar recursive data-constructing functions. The presenters demonstrate how TMC allows programmers to write code in a more natural style while maintaining the performance benefits of tail recursion. Learn about their formal verification approach using the Coq proof assistant and Iris base logic, where they prove the correctness of this compiler transformation in a simplified untyped calculus. The talk also highlights their extension of the Simuliris approach to support different calling conventions—the first application of Simuliris for proving compiler transformation correctness. The presentation includes references to the published article and supplementary materials, which have been evaluated as reusable artifacts.