A Certified Implementation of ML with Structural Polymorphism and Recursive Types

Jacques Garrigue. Mathematical Structures in Computer Science, November 2014, pages 1-25.

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.


Here are some older materials subsumed by the above work.

A Certified Implementation of ML with Structural Polymorphism.
In 8th Asian Symposium on Programming Languages and Systems, Shanghai, November 2010. A4 PDF.
Coq scripts for Coq 8.2pl2.
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.

JG 2014.11.14