[ 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
- 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.
- Mechanized monadic equational reasoning for ML references
- Reynald Affeldt, Jacques Garrigue and Takafumi Saikawa, HOPE
2024, Milano.
Slides,
Abstract,
Monae code.
2024.09.02