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:
- to introduce an abstraction barrier around the union-find mechanism of the
- to define a constraint language able to encode the core language
with polymorphic variants, and implement it using the current
- to write, or help writing, a monadic Gallina backend, so that at
least core ML programs (containing references) can be compiled.
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
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
Our current members are,
at Nagoya University:
and at AIST Tsukuba:
Developement takes place on
our GitHub group.