{"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":1775790711724,"version":"3.50.1"},"reference-count":26,"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:1006277616879","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"299-318","source":"Crossref","is-referenced-by-count":26,"title":["Type Inference Verified: Algorithm W in Isabelle\/HOL"],"prefix":"10.1007","volume":"23","author":[{"given":"Wolfgang","family":"Naraschewski","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"236904_CR1","unstructured":"Boutin, S.: Preuve de correction de la compilation de mini-ml en code cam dans le syst\u00e8me d'aide \u00e0 la d\u00e9monstration coq, Technical Report 2536, INRIA, Apr. 1995."},{"key":"236904_CR2","doi-asserted-by":"crossref","unstructured":"Burstall, R., MacQueen, D. and Sannella, D.: Hope: An experimental applicative language, in Proc. 1980 LISP Conference, 1980, pp. 136-143.","DOI":"10.1145\/800087.802799"},{"key":"236904_CR3","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, D., Despeyroux, J., Despeyroux, T. and Kahn, G.: A simple applicative language: Mini-ML, in Proc. ACM Conf. Lisp and Functional Programming, 1986, pp. 13-27.","DOI":"10.1145\/319838.319847"},{"key":"236904_CR4","doi-asserted-by":"crossref","unstructured":"Damas, L. and Milner, R.: Principal type schemes for functional programs, in Proc. 9th ACM Symp. Principles of Programming Languages, 1982, pp. 207-212.","DOI":"10.1145\/582153.582176"},{"key":"236904_CR5","unstructured":"Damas, L. M. M.: Type Assignment in Programming Languages, PhD Thesis, Department of Computer Science, University of Edinburgh, 1985."},{"key":"236904_CR6","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. de Bruijn","year":"1972","unstructured":"de Bruijn, N. G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math.\n34 (1972), 381-392.","journal-title":"Indag. Math."},{"key":"236904_CR7","doi-asserted-by":"crossref","unstructured":"Despeyroux, J., Pfenning, F. and Sch\u00fcrmann, C.: Primitive recursion for higher order abstract syntax, Technical Report CMU-CS-96-172, School of Computer Science, Carnegie Mellon University, 1996.","DOI":"10.1007\/3-540-62688-3_34"},{"key":"236904_CR8","unstructured":"Dubois, C. and M\u00e9nissier-Morain, V.: Certification of a type inference tool for ML: Damas-Milner within Coq, J. Automated Reasoning, this issue."},{"key":"236904_CR9","volume-title":"Introduction to HOL: A Theorem-Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M. and Melham, T.: Introduction to HOL: A Theorem-Proving Environment for Higher Order Logic, Cambridge Univ. Press, Cambridge, 1993."},{"key":"236904_CR10","doi-asserted-by":"crossref","unstructured":"Hannan, J. and Pfenning, F.: Compiler verification in LF, in 7th IEEE Symp. Logic in Computer Science, IEEE Computer Society Press, 1992, pp. 407-418.","DOI":"10.1109\/LICS.1992.185552"},{"key":"236904_CR11","first-page":"29","volume":"146","author":"J. R. Hindley","year":"1969","unstructured":"Hindley, J. R.: The principal type-scheme of an object in combinatory logic, Trans. AMS\n146 (1969), 29-60.","journal-title":"Trans. AMS"},{"key":"236904_CR12","doi-asserted-by":"crossref","unstructured":"Hudak, P., Jones, S. P. and Wadler, P.: Report on the programming language Haskell: A nonstrict, purely functional language, ACM SIGPLAN Notices\n27(5) (May 1992). Version 1.2.","DOI":"10.1145\/130697.130699"},{"key":"236904_CR13","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P. and Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification, in J.-L. Lassez and G. Plotkin (eds.), Computational Logic: Essays in Honor of Alan Robinson, MIT Press, 1991, pp. 257-321.","DOI":"10.1016\/0743-1066(92)90027-Z"},{"key":"236904_CR14","doi-asserted-by":"crossref","unstructured":"Lassez, J.-L., Maher, M. and Mariott, K.: Unification revisited, in J. Minker (ed.), Foundations of Deductive Databases and Logic Programming, Morgan Kaufman, 1987, pp. 587-625.","DOI":"10.1016\/B978-0-934613-40-8.50019-1"},{"key":"236904_CR15","doi-asserted-by":"crossref","unstructured":"McKinna, J. and Pollack, R.: Pure type systems formalized, in M. Bezem and J. Groote (eds.), Typed Lambda Calculi and Applications, LNCS 664, Springer-Verlag, 1993, pp. 289-305.","DOI":"10.1007\/BFb0037113"},{"key":"236904_CR16","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming, J. Comput. System Sci.\n17 (1978) 348-375.","journal-title":"J. Comput. System Sci."},{"key":"236904_CR17","unstructured":"Milner, R., Tofte, M. and Harper, R.: The Definition of Standard ML, MIT Press, 1990."},{"key":"236904_CR18","doi-asserted-by":"crossref","unstructured":"Naraschewski, W. and Nipkow, T.: Type inference verified: Algorithm W in Isabelle\/HOL, in E. Gim\u00e9nez and C. Paulin-Mohring (eds.), Types for Proofs and Programs: Intl. Workshop TYPES '96, LNCS 1512, Springer-Verlag, 1998, pp. 317-332.","DOI":"10.1007\/BFb0097799"},{"key":"236904_CR19","doi-asserted-by":"crossref","unstructured":"Nazareth, D. and Nipkow, T.: Formal verification of algorithm W: The monomorphic case, in J. von Wright, J. Grundy, and J. Harrison (eds.), Theorem Proving in Higher Order Logics, LNCS 1125, Springer-Verlag, 1996, pp. 331-346.","DOI":"10.1007\/BFb0105414"},{"key":"236904_CR20","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Functional unification of higher-order patterns, in 8th IEEE Symp. Logic in Computer Science, IEEE Computer Society Press, 1993, pp. 64-74.","DOI":"10.1109\/LICS.1993.287599"},{"issue":"2","key":"236904_CR21","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1017\/S0956796800001325","volume":"5","author":"T. Nipkow","year":"1995","unstructured":"Nipkow, T. and Prehofer, C.: Type reconstruction for type classes, J. Functional Programming\n5(2) (1995), 201-224.","journal-title":"J. Functional Programming"},{"key":"236904_CR22","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0167-6423(85)90009-7","volume":"5","author":"L. C. Paulson","year":"1985","unstructured":"Paulson, L. C.: Verifying the unification algorithm in LCF, Sci. of Computer Programming\n5 (1985), 143-169.","journal-title":"Sci. of Computer Programming"},{"key":"236904_CR23","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: Isabelle: A Generic Theorem Prover, LNCS 828, Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"236904_CR24","unstructured":"Paulson, L. C.: Generic automatic proof tools, in R. Veroff (ed.), Automated Reasoning and Its Applications, MIT Press, 1997. Also Report 396, Computer Laboratory, University of Cambridge."},{"key":"236904_CR25","unstructured":"Pfenning, F.: A proof of the Church-Rosser theorem and its representation in a logical framework, J. Automated Reasoning, to appear."},{"key":"236904_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M. Tofte","year":"1990","unstructured":"Tofte, M.: Type inference for polymorphic references, Inform. and Comput.\n89 (1990), 1-34.","journal-title":"Inform. and Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006277616879.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006277616879\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006277616879.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:35:43Z","timestamp":1749123343000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006277616879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,11]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999,11]]}},"alternative-id":["236904"],"URL":"https:\/\/doi.org\/10.1023\/a:1006277616879","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,11]]}}}