Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
summary
Formalizes OCaml GADT behavior by building a Coq mechanization of a core ML with structural polymorphism, recursive types and type-level equality; finds a principality bug in GADT pattern-match inference, fixes it by encoding ambivalent types and propagating rigidity via a graph representation of types, and is proving subject reduction as the first machine-checked metatheoretic result. Development reuses a certified ML base, avoids algorithmic unification by using sets of rigid unifiers, and work is ongoing.
AI-written summary · about