Abstract
We verify within the Coq proof assistant that ML ty** is sound with respect to the dynamic semantics. We prove this property in the framework of a big step semantics and also in the framework of a reduction semantics. For that purpose, we use a syntax-directed version of the ty** rules: we prove mechanically its equivalence with the initial type system provided by Damas and Milner. This work is complementary to the certification of the ML type inference algorithm done previously by the author and Valerie Ménissier-Morain.
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
B. Barras et al. The Coq Proof Assistant, Reference Manual, Version 6.1. INRIA, Rocquencourt, December 1996.
Samuel Boutin. Proving Correctness of the Translation from Mini-ML to the CAM with the Coq Proof Development System. Research report RR-2536, INRIA, Rocquencourt, April 1995.
Ana Bove. A Machine-assisted Proof that Well Typed Expressions Cannot Go Wrong. Chalmers University of Technology and Göteborg University, May 1998.
D. Clement, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple Applicative Language: Mini-ML. In Proceedings of the ACM Conference on Lisp and Functional Programming, August 1986. also available as research report RR-529, INRIA, Sophia-Antipolis, May 1986.
J. Despeyroux, F. Pfenning, C. Schürmann. Primitive Recursion for Higher-Order Abstract Syntax. In Proc. of TLCA’97, LNCS 1210, Springer Verlag, 1997.
C. Dubois, V. Ménissier-Morain. Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning, Vol 23, nos 3–4, 319–346, 1999.
C. Dubois, V. Viguié Donzeau-Gouge. A step towards the mechanization of partial functions: domains as inductive predicates. Workshop Mechanization of partial functions, CADE’15, Lindau, Germany, July 1998.
J. Frost. A Case Study of Co-induction in Isabelle. Technical Report 359, University of Cambridge, Computer Laboratory, February 1995.
R. Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990.
G. Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, Passau, Germany, 1987. Also available as a Research Report RR-601, Inria, Sophia-Antipolis, February 187.
H.P. Ko, M.E. Nadel. Substitution and refutation revisited. In K. Furukawa, editor, Proc. 8th International Conference on Logic Programming, 679–692, the MIT Press, 1991.
X. Leroy. Polymorphic ty** of an algorithmic language. Research report 1778, INRIA, 1992 (French original also available).
L. Damas, R. Milner. Principal type-schemes for functional programs. In Proceedings of the 15’th Annual Symposium on Principles of Programming Languages, pages 207–212. ACM, 1982.
T. Nipkow, D. von Oheimb. Javalight is Type-Safe-Definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, ACM Press, 1998, 161–170.
W. Naraschewski, T. Nipkow. Type Inference Verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, Vol 23, nos 3–4, 299–318, 1999.
S. Michaylov, F. Pfenning. Natural Semantics and some of its meta-theory in Elf. In Lars Halln, editor, Proceedings of the Second Workshop on Extensions of Logic Programming, Springer-Verlag LNCS, 1991. Also available as a Technical Report MPI-I-91-211, Max-Planck-Institute for Computer Science, Saarbrucken, Germany, August 1991.
O. Müller, K. Slind. Treating Partiality in a Logic of Total Functions. The Computer Journal, 40(10), 1997.
D. Rémy, J. Vouillon. An effective object-oriented extension to ML. Theory And Practice of Object Systems, 4(1):27–50, 1998.
D. Syme. Proving Java type soundness. Technical Report 427, University of Cambridge, Computer Laboratory, 1997.
D. Terrasse. Encoding Natural Semantics in Coq. In Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology (AMAST’95), LNCS 936. Springer-Verlag, July 1995.
D. Terrasse. Vers un Environnement d’Aide au Développement de Preuves en Sémantique Naturelle Thèse de Doctorat, Ecole Nationale des Ponts et Chaussées, 1995.
M. VanInwegen. Towards type preservation for core SML. University of Cambridge Computer Laboratory, 1997.
A. Wright, M. Felleisen. A Syntactic Approach to Type Soundness. Information and Computation, 115(1), pp.38–94, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dubois, C. (2000). Proving ML Type Soundness Within Coq. In: Aagaard, M., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2000. Lecture Notes in Computer Science, vol 1869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44659-1_9
Download citation
DOI: https://doi.org/10.1007/3-540-44659-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67863-2
Online ISBN: 978-3-540-44659-0
eBook Packages: Springer Book Archive