[ COCTI ]

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

Poster at PPL 2023 (in Japanese)
Code and proof scripts: cocti_defs.v test2.ml test2.v sortproof.v refproof.v
Typed Store Monad: monae/#105

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.

2023.11.26