COCTI : Certifiable OCaml Type Inference

COCTI is a 3 year project, supported by the Tezos Foundation, which aims at making OCaml type inference robust, modular, and verifiable.


Our short terms goals are Eventually, we would like to complete the following tasks:


Our current members are, at Nagoya University: and at AIST Tokyo Waterfront:


Developement takes place on our GitHub group.


Towards a Practical Library for Monadic Equational Reasoning in Coq
Ayumu Saito and Reynald Affeldt. 14th International Conference on Mathematics of Program Construction. Tbilisi, Georgia, September 2022. Volume 13544 of Springer LNCS, pages 151-177. Author's version.

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

Translation from OCaml to Coq and proof of programs
Kaoru Nakamura, Eito Maeda, Jacques Garrigue, Takafumi Saikawa. Poster presented at JSSST 2022. Poster (in Japanese)

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.

Towards a fully Prolog’ical typechecker
Jacques Garrigue and Takafumi Saikawa. Submitted. A4 paper.

Formalizing OCaml GADT typing in Coq
Jacques Garrigue and Xuanrui Qi. ML Workshop, Aug 2021. A4 paper.

Towards a Coq specification for generalized algebraic datatypes in OCaml
Xuanrui Qi and Jacques Garrigue. CoqPL Workshop, Jan 2021. A4 paper.

A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. Journal of Functional Programming 31:e17, 2021. Author's version.