{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:56:19Z","timestamp":1770285379434,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540615873","type":"print"},{"value":"9783540706410","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105414","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"331-345","source":"Crossref","is-referenced-by-count":5,"title":["Formal verification of algorithm W: The monomorphic case"],"prefix":"10.1007","author":[{"given":"Dieter","family":"Nazareth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/0167-6423(87)90019-0","volume":"8","author":"L. Cardelli","year":"1987","unstructured":"L. Cardelli. Basic polymorphic typechecking. Sci. Comp. Programming, 8:147\u2013172, 1987.","journal-title":"Sci. Comp. Programming"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"D. Cl\u00e9ment, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple applicative language: Mini-ML. In Proc. ACM Conf. Lisp and Functional Programming, pages 13\u201327, 1986.","DOI":"10.1145\/319838.319847"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"L. Damas and R. Milner. Principal type schemes for functional programs. In Proc. 9th ACM Symp. Principles of Programming Languages, pages 207\u2013212, 1982.","DOI":"10.1145\/582153.582176"},{"key":"22_CR4","unstructured":"L. M. M. Damas. Type Assignment in Programming Languages. PhD thesis, Department of Computer Science, University of Edinburgh, 1985."},{"key":"22_CR5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. Bruijn de","year":"1972","unstructured":"N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381\u2013392, 1972.","journal-title":"Indagationes Mathematicae"},{"key":"22_CR6","unstructured":"M. Gordon and T. Melham. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993."},{"key":"22_CR7","doi-asserted-by":"publisher","first-page":"29","DOI":"10.2307\/1995158","volume":"146","author":"J. R. Hindley","year":"1969","unstructured":"J. R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc., 146:29\u201360, 1969.","journal-title":"Trans. Amer. Math. Soc."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"P. Hudak, S. Peyton Jones, and P. Wadler. Report on the programming language Haskell: A non-strict, purely functional language. ACM SIGPLAN Notices, 27(5), May 1992. Version 1.2.","DOI":"10.1145\/130697.130699"},{"key":"22_CR9","unstructured":"M. P. Jones. Qualified Types: Theory and Practice. Technical Monograph PRG-106, Oxford University Computing Laboratory, Programming Research Group, July 1992."},{"key":"22_CR10","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 257\u2013321. MIT Press, 1991."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"J.-L. Lassez, M. Maher, and K. Mariott. Unification revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587\u2013625. Morgan Kaufman, 1987.","DOI":"10.1016\/B978-0-934613-40-8.50019-1"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lect. Notes in Comp. Sci., pages 289\u2013305. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0037113"},{"key":"22_CR14","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, 17:348\u2013375, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"22_CR15","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990."},{"key":"22_CR16","unstructured":"D. Nazareth. A Polymorphic Sort System for Axiomatic Specification Languages. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, 1995. Technical Report TUM-I9515."},{"issue":"2","key":"22_CR17","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1017\/S0956796800001325","volume":"5","author":"T. Nipkow","year":"1995","unstructured":"T. Nipkow and C. Prehofer. Type reconstruction for type classes. J. Functional Programming, 5(2):201\u2013224, 1995.","journal-title":"J. Functional Programming"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"22_CR19","unstructured":"L. C. Paulson. Generic automatic proof tools. Technical Report 396, University of Cambridge, Computer Laboratory, 1996."},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"R. Pollack. A verified typechecker. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lect. Notes in Comp. Sci. Springer-Verlag, 1995.","DOI":"10.1007\/BFb0014065"},{"key":"22_CR21","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"J. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12:23\u201341, 1965.","journal-title":"J. ACM"},{"key":"22_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M. Tofte","year":"1990","unstructured":"M. Tofte. Type inference for polymorphic references. Information and Computation, 89:1\u201334, 1990.","journal-title":"Information and Computation"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"P. Wadler. Comprehending monads. In Conference on Lisp and Functional Programming, pages 61\u201378, June 1990.","DOI":"10.1145\/91556.91592"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"P. Wadler. The essence of functional programming. In Proc. 19th ACM Symp. Principles of Programming Languages, 1992.","DOI":"10.1145\/143165.143169"},{"key":"22_CR25","doi-asserted-by":"crossref","first-page":"115","DOI":"10.3233\/FI-1987-10202","volume":"10","author":"M. Wand","year":"1987","unstructured":"M. Wand. A simple algorithm and proof for type inference. Fundementa Informaticae, 10:115\u2013122, 1987.","journal-title":"Fundementa Informaticae"}],"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\/BFb0105414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T22:52:14Z","timestamp":1639608734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105414"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0105414","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}