Interpreting OCaml GADTs into Coq
summary
Implements a two-pronged translation that maps OCaml GADT indices to an intensional ML-type syntax and then interprets those into concrete Coq types so reduction remains computable; produces explicit equality witnesses that let Coq accept functions like head on length-indexed vectors and proves constructor injectivity for indices. Integrates with the existing Cogen backend, needs a compiler trace of generated equations, handles many core-ML features but still fails for existentially split indices and proposes a relation-based workaround.
AI-written summary · about
chapters (8)
- 0:00Starting point: the Coggen project
- 1:12Soundness by translation
- 3:04A classical example
- 4:58What about head?
- 6:52The difference between GADTs and inductive types
- 10:29Type interpretation function
- 12:49Injectivity of type constructors
- 14:14Mixed use of existential type variables
related talks
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
29mMechanized monadic equational reasoning for ML references
24mCode Extraction from Coq to ML-like languages
21mTail Modulo Cons, OCaml, and Relational Separation Logic
46mMechanizing Abstract Interpretation
26mAn Invitation to OCaml