Implementing OCaml APIs in Coq
summary
Extraction is modified to map Coq encodings of OCaml effects to real OCaml exceptions and refs so extracted code matches existing APIs while remaining executable in Coq and OCaml. The repo includes a small library and three worked examples: List.head implemented via an error monad that extracts to OCaml exceptions, a mutable counter using a state module with fixed initial value that extracts to refs, and a stateful term API with fresh-name generation proved correct using reflective VM computation and shallow-state lemmas. Limitations: some manual extraction wiring, dune pre-processing, and client-opacity risks.
AI-written summary · about
chapters (8)
- 0:00OCaml APIs in Coq intro
- 2:29OCaml API challenges in Coq
- 5:17Modeling exceptions with error monad
- 8:25Handling mutable state in Coq
- 10:50Reasoning about stateful computations
- 13:58Related work and limits
- 15:41Summary and future
- 16:06Q&A
related talks
21mVerified Extraction from Coq to OCaml
24mCode Extraction from Coq to ML-like languages
19mInterpreting OCaml GADTs into Coq
29mMechanized monadic equational reasoning for ML references
15mEfficient Compilation of Algebraic Effect Handlers
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
21mTail Modulo Cons, OCaml, and Relational Separation Logic
24mOn the design and implementation of Modular Explicits