Coqgen : A Coq generation backend for OCaml

Coqgen (aka ocaml_in_coq) is a backend for OCaml that generates well-typed and executable Coq code. Its main goal is proving the ensuring the type-soundness of OCaml code by re-checking in Coq, but another application is proving properties OCaml programs based on a precise semantics. We describe here works related to this project.
A Gallina generating backend to check OCaml's type inference correctness
Jacques Garrigue, Takafumi Saikawa.
TYPES 2022, Nantes. Abstract, Slides, Code.
PPL 2022. Poster.
TPP 2021, Kitami. Slides.

Proving the correctness of OCaml programs translated into Coq / OCaml プログラムの Coq への変換とプログラムの正しさの証明
Eito Maida, Kaoru Nakamura, Takafumi Saikawa and Jacques Garrigue
毎田詠人, 中村薫, 才川隆文, Jacques Garrigue

Interpreting OCaml GADTs into Coq
Jacques Garrigue and Takafumi Saikawa. ML Workshop 2022, Ljubljana. Slides, Abstract, ML Code, Coq Code.

Environment-friendly monadic equational reasoning for OCaml
Reynald Affeldt, Jacques Garrigue and Takafumi Saikawa, Coq Workshop 2023, Bialystok. (and TPP 2023, Titech) Coq WS Slides, TPP Slides, NIER Slides, Abstract, Monae code.