A certified implementation of ML with structural polymorphism and recursive types

摘要

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