Tail Modulo Cons, OCaml, and Relational Separation Logic
summary
Implements Tail Modulo Constructor in the OCaml compiler and shows it reliably turns non‑tail List.map‑style definitions into stack‑safe code; proof of correctness is mechanized in Coq + Iris and checks a simplified untyped calculus that captures the real implementation details. Introduces a Simuliris‑based extension to relate differing calling conventions (used to verify destination‑passing style), ships reusable artifacts, and reports the transformation working in the compiler with machine‑checked proofs.
AI-written summary · about
chapters (5)
- 0:00TMC and OCaml intro
- 14:53Changing calling conventions
- 15:36Proof specs for transforms
- 19:11Implementation and verification
- 19:56Q&A concurrency Simaris
related talks
30mTail Modulo Async/Await
27mTail Recursion Modulo Context: An Equational Approach
19mInterpreting OCaml GADTs into Coq
24mOn the design and implementation of Modular Explicits
19mExtensible Metatheory Mechanization via Family Polymorphism
20mModern DSL compiler architecture in OCaml our experience with Catala
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
15mCompiling with Continuations, Correctly