Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
summary
A Coq mechanization of OCaml-style GADTs targets a core language with structural polymorphism, recursive types and type-level equality witnesses (OCaml 4.11). The development proves soundness fragments and aims for subject reduction, exposes a real principality bug: witness-opening order makes ambivalence escape inference, breaking principality. Fix uses a graph representation with rigid-variable annotations to propagate ambivalence. Implementation reuses a certified ML base, avoids algorithmic unification, finishes substitution lemmas, and leaves some subject-reduction cases and freshness automation to finish.
AI-written summary · about
chapters (5)
related talks
19mInterpreting OCaml GADTs into Coq
18mThe Essence of Generalized Algebraic Data Types
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
19mExtensible Metatheory Mechanization via Family Polymorphism
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
29mMechanized monadic equational reasoning for ML references
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
59mCoq to C Translation with Partial Evaluation + Counterexample Generation