{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:51Z","timestamp":1775790711764,"version":"3.50.1"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1999,11]]},"DOI":"10.1023\/a:1006285817788","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"319-346","source":"Crossref","is-referenced-by-count":13,"title":["Certification of a Type Inference Tool for ML: Damas\u2013Milner within Coq"],"prefix":"10.1007","volume":"23","author":[{"given":"Catherine","family":"Dubois","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Val\u00e9rie","family":"M\u00e9nissier-Morain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"236906_CR1","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filli\u00e2tre, J., Gim\u00e9nez, E., Herbelin, H., Huet, G., Manoury, P., Mu\u00f1oz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Sa\u00efbi, A. and Werner, B.: The Coq proof assistant, reference manual, Version 6.1, INRIA, Rocquencourt, December 1996. Also available at http:\/\/pauillac.inria.fr\/coq\/doc\/main.html."},{"key":"236906_CR2","unstructured":"Boutin, S.: Proving correctness of the translation from mini-ML to the CAMwith the Coq proof development system, Research Report RR-2536, INRIA, Rocquencourt, April 1995."},{"key":"236906_CR3","doi-asserted-by":"crossref","unstructured":"Clement, D., Despeyroux, J., Despeyroux, T. and Kahn, G.: 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":"236906_CR4","doi-asserted-by":"crossref","unstructured":"Damas, L. and Milner, R.: Principal type-schemes for functional programs, in Proceedings of the 15th Annual Symposium on Principles of Programming Languages, ACM, 1982, pp. 207-212.","DOI":"10.1145\/582153.582176"},{"key":"236906_CR5","unstructured":"Dubois, C.: S\u00fbret\u00e9 du typage de ML: Sp\u00e9cification et Preuve en Coq. 9\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs, C\u00f4me, Italie, 1998."},{"key":"236906_CR6","unstructured":"Dubois, C. and M\u00e9nissier-Morain, V.: A proved type inference tool for ML: Damas-Milner within Coq (work in progress), in J. von Wright, J. Grundy and J. Harrison (eds.), Supplementary Proceedings of Theorem Proving in Higher Order Logics, Turku Centre for Computer Science, 1996, pp. 15-30."},{"key":"236906_CR7","doi-asserted-by":"crossref","unstructured":"Dubois, C., Rouaix, F. and Weis, P.: Extensional polymorphism, in Proceedings of the 22th ACM Conference on Principles of Programming Languages, January 1995, pp. 118-129.","DOI":"10.1145\/199448.199473"},{"key":"236906_CR8","unstructured":"Dubois, C. and Vigui\u00e9 Donzeau-Gouge, V.: A step towards the mechanization of partial functions: Domains as inductive predicates, CADE-15, Workshop on Mechanization of Partial Functions, Lindau, 1998."},{"key":"236906_CR9","unstructured":"Jaume, M.: Unification: A case study in transposition of formal properties, in E. L. Gunter and A. Felty (eds.), Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics: Poster Session TPHOLs'97, Murray Hill, NJ, 1997, pp. 79-93."},{"key":"236906_CR10","unstructured":"Kahn, G.: Natural semantics, in Proceedings of the Symposium on Theoretical Aspects of Computer Science, 1987."},{"key":"236906_CR11","unstructured":"Leroy, X.: Polymorphic typing of an algorithmic language. Research Report (English version of his Ph.D. Thesis at Universit\u00e9 Paris 7) RR-1778, INRIA, Rocquencourt, 1992."},{"key":"236906_CR12","unstructured":"Naraschewski, W. and Nipkow, T.: Type inference verified: Algorithm W in Isabelle\/HOL, J. Automated Reasoning, this issue."},{"key":"236906_CR13","doi-asserted-by":"crossref","unstructured":"Nazareth, D. and Nipkow, T.: Formal verification of algorithm W: The monomorphic case, in Proceedings of Theorem Proving in Higher Order Logics, LNCS 1125, Springer-Verlag, 1996, pp. 331-345.","DOI":"10.1007\/BFb0105414"},{"key":"236906_CR14","doi-asserted-by":"crossref","unstructured":"Parent, C.: Developing certified programs in Coq - The program tactic, in H. Barendregt and T. Nipkow (eds.), Proceedings of the International Workshop on Types for Proofs and Programs, LNCS 806, Springer-Verlag, 1993, pp. 291-312.","DOI":"10.1007\/3-540-58085-9_81"},{"key":"236906_CR15","doi-asserted-by":"crossref","unstructured":"Pfenning, F. and Paulin-Mohring, C.: Inductively defined types in the calculus of constructions, in Proceedings of Mathematical Foundations of Programming Semantics, LNCS 442, Springer-Verlag 1990.","DOI":"10.1007\/BFb0040259"},{"key":"236906_CR16","unstructured":"Rouyer, J.: D\u00e9veloppement de l'algorithme d'unification dans le calcul des constructions avec types inductifs, INRIA-Lorraine, Research Report 1795, November 1992."},{"key":"236906_CR17","doi-asserted-by":"crossref","unstructured":"Terrasse, D.: 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.","DOI":"10.1007\/3-540-60043-4_56"},{"key":"236906_CR18","doi-asserted-by":"crossref","unstructured":"Wright, A. K.: Simple imperative polymorphism, Lisp and Symbolic Computation, 1994.","DOI":"10.1007\/BF01018828"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006285817788.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006285817788\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006285817788.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:44:16Z","timestamp":1749123856000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006285817788"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,11]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999,11]]}},"alternative-id":["236906"],"URL":"https:\/\/doi.org\/10.1023\/a:1006285817788","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,11]]}}}