A Certified Implementation of ML with Structural Polymorphism

Abstract. The type system of Objective Caml has many unique features, which make ensuring the correctness of its implementation difficult. One of these features is structurally polymorphic types, such as polymorphic object and variant types, which have the extra specificity of allowing recursion. We implemented in Coq a certified interpreter for Core ML extended with structural polymorphism and recursion. Along with type soundness of evaluation, soundness and principality of type inference, and correctness of a stack-based interpreter, are also proved.

• A4 PDF version of this paper.
• Long PDF revised version of this paper. Submitted, February 2012.
• Coq scripts for the proofs, allowing extraction of a certified algorithm.

Here are some older materials subsumed by the above work.

A Certified Interpreter for ML with Structural Polymorphism.

Presented at WMM'09, Edingurgh, Scotland. Extended abstract: A4 PDF.

Coq scripts for the proofs, allowing extraction of a certified algorithm.

Type inference for structural polymorphism

Slides from a presentation at TPP08 (Sendai, 2008-11-26): A4 PDF.

Coq scripts for the proofs, allowing extraction of a certified algorithm.

Proving OCaml's type system?

Slides from a presentation at INRIA (Rocquencourt, 2008-06-13): A4 PDF.

Coq scripts for structural polymorphism extended with Kind GC (updated 2008-06-20).

A formal proof of soundness for structural polymorphism

Coq scripts proving the soundness described in Simple type inference for structural polymorphism, based on Arthur Charguéraud et al. Engineering Formal Metatheory.

Slides from a presentation at TPP07 (Tsukuba, 2007-11-22): A4 PDF.