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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proc. ACM Symposium on Principles of Programming Languages, pp. 3–15 (2008)
Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005)
Barras, B.: Auto-validation d’un système de preuves avec familles inductives. Thèse de doctorat, Université Paris 7 (November 1999)
Crary, K., Harper, B.: Mechanized definition of Standard ML alpha release. Twelf proof scripts (August 2009)
Dubois, C.: Proving ML type soundness within Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 126–144. Springer, Heidelberg (2000)
Dubois, C., Ménissier-Morain, V.: Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning 23(3), 319–346 (1999)
Furuse, J.P., Garrigue, J.: A label-selective lambda-calculus with optional arguments and its compilation method. RIMS Preprint 1041, Research Institute for Mathematical Sciences, Kyoto University (October 1995)
Garrigue, J.: Simple type inference for structural polymorphism. In: The Ninth International Workshop on Foundations of Object-Oriented Languages, Portland, Oregon (2002)
Garrigue, J.: Relaxing the value restriction. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, Springer, Heidelberg (2004)
Garrigue, J., Rémy, D.: Extending ML with semi-explicit higher order polymorphism. Information and Computation 155, 134–171 (1999)
Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of standard ML. In: Proc. ACM Symposium on Principles of Programming Languages, pp. 173–184 (January 2007)
Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system release 3.11, Documentation and user’s manual. Projet Gallium, INRIA (November 2008)
Naraschewski, W., Nipkow, T.: Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning 23, 299–318 (1999)
Oheimb, D.v., Nipkow, T.: Machine-checking the Java specification: Proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 119–156. Springer, Heidelberg (1999)
Owens, S.: A sound semantics for OCaml light. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 1–15. Springer, Heidelberg (2008)
Paulson, L.: Verifying the unification algorithm in LCF. Science of Computer Programming 5, 143–169 (1985)
The Coq Team. The Coq Proof Assistant, Version 8.2. INRIA (2009)
Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In: Proc. ACM Symposium on Principles of Programming Languages (2008)
Urban, C., Nipkow, T.: Nominal verification of algorithm W. In: Huet, G., Lévy, J.-J., Plotkin, G. (eds.) From Semantics to Computer Science. Essays in Honour of Gilles Kahn, pp. 363–382. Cambridge University Press, Cambridge (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garrigue, J. (2010). A Certified Implementation of ML with Structural Polymorphism. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-17164-2_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17163-5
Online ISBN: 978-3-642-17164-2
eBook Packages: Computer ScienceComputer Science (R0)