MetaOCaml Theory and Implementation
summary
An integrated translation in BER MetaOCaml N114 interleaves quotation/antiquotation lowering with OCaml type checking so the compiler no longer rebuilds whole ASTs for non‑staged code, uses a global stage stored on value attributes, and produces combinator calls that eventually remove all brackets and escapes. The paper claims and proves a type‑preserving translation and that all escapes are eliminated, and reports a working implementation in MetaOCaml (May release) with backends to C/wasm/OpenCL.
AI-written summary · about
chapters (6)
related talks
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
32mMacoCaml: Staging Composable and Compilable Macros
15mEfficient Compilation of Algebraic Effect Handlers
24mCode Extraction from Coq to ML-like languages
15mType-safe generation of modules in applicative and generative styles
19mInterpreting OCaml GADTs into Coq
26mAn Invitation to OCaml
21mVerified Extraction from Coq to OCaml