COCTI : Certifiable OCaml Type Inference

Goals

• 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.

• 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

• Jacques Garrigue (github)
• Xuanrui Qi (github)
• Takafumi Saikawa (github)

• Reynald Affeldt (github)

Activity