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.

Goals

Our short terms goals are

to introduce an abstraction barrier around the union-find mechanism of the compiler;
to define a constraint language able to encode the core language with polymorphic variants, and implement it using the current resolution mechanisms;
to write, or help writing, a monadic Gallina backend, so that at least core ML programs (containing references) can be compiled.

Eventually, we would like to complete the following tasks:

Rewrite OCaml type inference engine using state of the art techniques, such as separating constraint generation and solving, and redefine the output of type inference to make it amenable to integrity checking and program transformation.
Modularize the OCaml type checker using constraint-based type inference and certify it using the Coq proof assistant.
Provide an alternative backend for OCaml, generating monadic Gallina code (i.e. programs to be type-checked by Coq), in a style close to OCaml’s lambda intermediate language for machine-checked verification.

Members

Our current members are, at Nagoya University:

Jacques Garrigue (github)
Hyunggyu Jang (github)
Eito Maida (github)
Kaoru Nakamura (github)
Xuanrui Qi (github)
Takafumi Saikawa (github)

and at AIST Tokyo Waterfront:

Reynald Affeldt (github)

Activity

Developement takes place on our GitHub group. Most of the code is in COCTI/ocaml, our clone of the ocaml repository. We have been working in 4 directions

Rewriting and refactoring parts of the OCaml type checker
Proving the soundness of the type theory underlying OCaml
Developing a Coq backend for OCaml: Coqgen
Developing techniques to prove the correctness of programs

Publications

Environment-friendly monadic equational reasoning for OCaml: Reynald Affeldt, Jacques Garrigue and Takafumi Saikawa, Coq Workshop 2023, Bialystok. Coq WS Slides, TPP Slides, Abstract, Monae code, Coqgen.
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); Poster presented at PPL 2023. 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.

2023.10.30