MacoCaml: Staging Composable and Compilable Macros
summary
MacoCaml implements compile‑time code generation inside the OCaml compiler, treating macros as compile-time bindings and using quotation/splice staging so compile evaluation runs only in top-level splices. The work formalizes a typed calculus maco with references and modules, proves type soundness and a novel phase distinction theorem that compile-time state cannot leak to runtime, and ships an implementation with artifacts evaluated and two nontrivial libraries ported (stream fusion and formatting) to validate the design.
AI-written summary · about
chapters (5)
- 0:00MacroCaml introduction
- 1:50Staging and macros unified
- 10:00Macro calculus formalization
- 17:53Implementation and porting
- 23:08Summary and Q&A
related talks
12mMulti-Stage Programming with Generative and Analytical Macros
42mThe Macronomicon
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
29mMetaOCaml Theory and Implementation
27mDo You Even Macro?
48mMetaprogramming in Dotty
06mCode Generation: The Lisp Way
14mType-Sensitive Algebraic Macros