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 are also proved. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Garrigue, J. (2010). A certified implementation of ML with structural polymorphism. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6461 LNCS, pp. 360–375). https://doi.org/10.1007/978-3-642-17164-2_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
