Sciweavers

Share
APLAS
2010
ACM

A Certified Implementation of ML with Structural Polymorphism

10 years 3 months ago
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. I 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 are also proved.
Jacques Garrigue
Added 05 Dec 2010
Updated 05 Dec 2010
Type Conference
Year 2010
Where APLAS
Authors Jacques Garrigue
Comments (0)
books