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
2019.11.15