{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T12:20:50Z","timestamp":1753273250244},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_9","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"126-144","source":"Crossref","is-referenced-by-count":11,"title":["Proving ML Type Soundness Within Coq"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Dubois","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"B. Barras et al. The Coq Proof Assistant, Reference Manual, Version 6.1. INRIA, Rocquencourt, December 1996."},{"key":"9_CR2","series-title":"Research report","volume-title":"Proving Correctness of the Translation from Mini-ML to the CAM with the Coq Proof Development System","author":"S. Boutin","year":"1995","unstructured":"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."},{"key":"9_CR3","unstructured":"Ana Bove. A Machine-assisted Proof that Well Typed Expressions Cannot Go Wrong. Chalmers University of Technology and G\u00f6teborg University, May 1998."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/319838.319847"},{"key":"9_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of TLCA\u201997","author":"J. Despeyroux","year":"1997","unstructured":"J. Despeyroux, F. Pfenning, C. Sch\u00fcrmann. Primitive Recursion for Higher-Order Abstract Syntax. In Proc. of TLCA\u201997, LNCS 1210, Springer Verlag, 1997."},{"issue":"3\u20134","key":"9_CR6","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1006285817788","volume":"23","author":"C. Dubois","year":"1999","unstructured":"C. Dubois, V. M\u00e9nissier-Morain. Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning, Vol 23, nos 3\u20134, 319\u2013346, 1999.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR7","unstructured":"C. Dubois, V. Vigui\u00e9 Donzeau-Gouge. A step towards the mechanization of partial functions: domains as inductive predicates. Workshop Mechanization of partial functions, CADE\u201915, Lindau, Germany, July 1998."},{"key":"9_CR8","unstructured":"J. Frost. A Case Study of Co-induction in Isabelle. Technical Report 359, University of Cambridge, Computer Laboratory, February 1995."},{"key":"9_CR9","series-title":"Technical Report","volume-title":"Systems of polymorphic type assignment in LF","author":"R. Harper","year":"1990","unstructured":"R. Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990."},{"key":"9_CR10","unstructured":"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."},{"key":"9_CR11","unstructured":"H.P. Ko, M.E. Nadel. Substitution and refutation revisited. In K. Furukawa, editor, Proc. 8th International Conference on Logic Programming, 679\u2013692, the MIT Press, 1991."},{"key":"9_CR12","unstructured":"X. Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA, 1992 (French original also available)."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"L. Damas, R. Milner. Principal type-schemes for functional programs. In Proceedings of the 15\u2019th Annual Symposium on Principles of Programming Languages, pages 207\u2013212. ACM, 1982.","DOI":"10.1145\/582153.582176"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"T. Nipkow, D. von Oheimb. Javalight is Type-Safe-Definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, ACM Press, 1998, 161\u2013170.","DOI":"10.1145\/268946.268960"},{"issue":"3\u20134","key":"9_CR15","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1023\/A:1006277616879","volume":"23","author":"W. Naraschewski","year":"1999","unstructured":"W. Naraschewski, T. Nipkow. Type Inference Verified: Algorithm W in Isabelle\/HOL. Journal of Automated Reasoning, Vol 23, nos 3\u20134, 299\u2013318, 1999.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Second Workshop on Extensions of Logic Programming","author":"S. Michaylov","year":"1991","unstructured":"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."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller, K. Slind. Treating Partiality in a Logic of Total Functions. The Computer Journal, 40(10), 1997.","DOI":"10.1093\/comjnl\/40.10.640"},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1002\/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4","volume":"4","author":"D. R\u00e9my","year":"1998","unstructured":"D. R\u00e9my, J. Vouillon. An effective object-oriented extension to ML. Theory And Practice of Object Systems, 4(1):27\u201350, 1998.","journal-title":"Theory And Practice of Object Systems"},{"key":"9_CR19","unstructured":"D. Syme. Proving Java type soundness. Technical Report 427, University of Cambridge, Computer Laboratory, 1997."},{"key":"9_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology (AMAST\u201995)","author":"D. Terrasse","year":"1995","unstructured":"D. Terrasse. Encoding Natural Semantics in Coq. In Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology (AMAST\u201995), LNCS 936. Springer-Verlag, July 1995."},{"key":"9_CR21","unstructured":"D. Terrasse. Vers un Environnement d\u2019Aide au D\u00e9veloppement de Preuves en S\u00e9mantique Naturelle Th\u00e8se de Doctorat, Ecole Nationale des Ponts et Chauss\u00e9es, 1995."},{"key":"9_CR22","unstructured":"M. VanInwegen. Towards type preservation for core SML. University of Cambridge Computer Laboratory, 1997."},{"issue":"1","key":"9_CR23","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A. Wright","year":"1994","unstructured":"A. Wright, M. Felleisen. A Syntactic Approach to Type Soundness. Information and Computation, 115(1), pp.38\u201394, 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T01:16:29Z","timestamp":1550452589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}