Implementing OCaml APIs in Coq

Learn about a lightweight design pattern for implementing OCaml APIs in Coq in this 19-minute conference talk from CoqPL 2025 by Joshua M. Cohen of Princeton University. The presentation addresses the challenge of preserving exact types and behaviors when implementing stateful, exception-throwing OCaml APIs through extraction. Discover how carefully modified extraction can support features like exceptions and mutable state, resulting in programs that are executable both within Coq and in OCaml while maintaining complete compatibility with client expectations. The talk demonstrates this approach through three examples: a subset of OCaml's List library, a mutable counter, and a stateful term API for generating unique variable names for α-conversion and safe substitution. This research was presented at the CoqPL 2025 workshop on January 25, 2025, sponsored by ACM SIGPLAN.