{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T13:11:25Z","timestamp":1777036285382,"version":"3.51.4"},"reference-count":55,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1996,7,1]],"date-time":"1996-07-01T00:00:00Z","timestamp":836179200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":6225,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[1996,7]]},"DOI":"10.1016\/0167-6423(95)00007-0","type":"journal-article","created":{"date-parts":[[2002,10,31]],"date-time":"2002-10-31T16:12:04Z","timestamp":1036080724000},"page":"37-83","source":"Crossref","is-referenced-by-count":57,"title":["Explaining type inference"],"prefix":"10.1016","volume":"27","author":[{"given":"Dominic","family":"Duggan","sequence":"first","affiliation":[]},{"given":"Frederick","family":"Bent","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0167-6423(95)00007-0_BIB1","series-title":"Compilers: Principles, Techniques and Tools","author":"Aho","year":"1986"},{"key":"10.1016\/0167-6423(95)00007-0_BIB2","series-title":"The Warren Abstract Machine","author":"Ait-Kaci","year":"1991"},{"key":"10.1016\/0167-6423(95)00007-0_BIB3","series-title":"Proc. Symp. on Programming Language Implementation and Logic Programming","first-page":"1","article-title":"Standard ML of New Jersey","volume":"Volume. 528","author":"Appel","year":"1991"},{"key":"10.1016\/0167-6423(95)00007-0_BIB4","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1145\/6465.20890","article-title":"The PSG system: From formal language definitions to interactive program environments","volume":"8","author":"Bahlke","year":"1986","journal-title":"ACM Trans. Programming Languages Systems"},{"key":"10.1016\/0167-6423(95)00007-0_BIB5","article-title":"An efficient unification algorithm","author":"Baxter","year":"1973"},{"key":"10.1016\/0167-6423(95)00007-0_BIB6","article-title":"The complexity of unification","author":"Baxter","year":"1976"},{"key":"10.1016\/0167-6423(95)00007-0_BIB7","article-title":"An ML type error explanation system","author":"Bent","year":"1994"},{"key":"10.1016\/0167-6423(95)00007-0_BIB8","series-title":"Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation","first-page":"192","article-title":"Type inference in the presence of type abstraction","author":"Boehm","year":"1989"},{"key":"10.1016\/0167-6423(95)00007-0_BIB9","series-title":"Proc. ACM SIGSOFT\/SIGPLAN Symp. on Practical Software Development Environments","first-page":"14","article-title":"Centaur: The system","author":"Borras","year":"1988"},{"key":"10.1016\/0167-6423(95)00007-0_BIB10","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/0167-6423(87)90019-0","article-title":"Basic polymorphic typechecking","volume":"8","author":"Cardelli","year":"1987","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0167-6423(95)00007-0_BIB11","series-title":"Information Processing: Proc. IFIP World Congr.","first-page":"909","article-title":"A rehabilitation of Robinson's unification algorithm","author":"Corbin","year":"1983"},{"issue":"32","key":"10.1016\/0167-6423(95)00007-0_BIB12","first-page":"79","article-title":"About the Paterson-Wegman linear unification algorithm","volume":"32","author":"de Champeaux","year":"1985","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/0167-6423(95)00007-0_BIB13","unstructured":"D. Duggan, Verified type explanation, In preparation."},{"key":"10.1016\/0167-6423(95)00007-0_BIB14","unstructured":"D. Duggan, Efficient subtype inference, In preparation."},{"key":"10.1016\/0167-6423(95)00007-0_BIB15","unstructured":"D. Duggan, A type inference explanation facility for ML, In preparation."},{"key":"10.1016\/0167-6423(95)00007-0_BIB16","article-title":"Kinded parametric overloading","author":"Duggan","year":"1994"},{"key":"10.1016\/0167-6423(95)00007-0_BIB17","series-title":"Topics in Advanced Language Implementation","first-page":"289","article-title":"A semi-functional implementation of a higher-order logic programming language","author":"Elliott","year":"1991"},{"key":"10.1016\/0167-6423(95)00007-0_BIB18","article-title":"Type checking and type deduction in polymorphic programming languages","author":"Giannini","year":"1985"},{"key":"10.1016\/0167-6423(95)00007-0_BIB19","series-title":"Functional Programming, Workshops in Computing","first-page":"146","article-title":"Efficient type inference using monads","author":"Hammond","year":"1991"},{"key":"10.1016\/0167-6423(95)00007-0_BIB20","article-title":"Recherches sur la Theorie de la Demonstration (these)","author":"Herbrand","year":"1930"},{"key":"10.1016\/0167-6423(95)00007-0_BIB21","article-title":"The G\u00f6del programming language","author":"Hill","year":"1992"},{"issue":"5","key":"10.1016\/0167-6423(95)00007-0_BIB22","doi-asserted-by":"crossref","DOI":"10.1145\/130697.130699","article-title":"Report on the programming language Haskell, a non-strict purely functional language","volume":"27","author":"Hudak","year":"1992","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/0167-6423(95)00007-0_BIB23","article-title":"Resolutions d'equations dans les langages d'ordre 1,2,\u2026,\u03c9","author":"Huet","year":"1976"},{"key":"10.1016\/0167-6423(95)00007-0_BIB24","series-title":"Message on haskell electronic mailing list","author":"Hughes","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB25","series-title":"Proc. ACM Symp. on Principles of Programming Languages","first-page":"44","article-title":"A maximum-flow approach to anomaly isolation in unification-based incremental type inference","author":"Johnson","year":"1986"},{"key":"10.1016\/0167-6423(95)00007-0_BIB26","series-title":"Symp. on Theoretical Aspects of Computer Science","first-page":"22","article-title":"Natural semantics","volume":"Vol. 247","author":"Kahn","year":"1987"},{"key":"10.1016\/0167-6423(95)00007-0_BIB27","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/62029.62030","article-title":"Unification: A multidisciplinary survey","volume":"21","author":"Knight","year":"1989","journal-title":"ACM Comput. Surveys"},{"key":"10.1016\/0167-6423(95)00007-0_BIB28","series-title":"1st. di Elaborazione delle Informazione","article-title":"Unification in linear time and space: a structured presentation","author":"Martelli","year":"1976"},{"key":"10.1016\/0167-6423(95)00007-0_BIB29","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM Trans. Programming Languages Systems"},{"key":"10.1016\/0167-6423(95)00007-0_BIB30","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","article-title":"A logic programming language with lambda-abstraction, function variables and simple unification","volume":"1","author":"Miller","year":"1991","journal-title":"J. Logic Comput."},{"key":"10.1016\/0167-6423(95)00007-0_BIB31","series-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"10.1016\/0167-6423(95)00007-0_BIB32","series-title":"Types in Logic Programming","first-page":"245","article-title":"Types in higher order logic programming","author":"Nadathur","year":"1992"},{"key":"10.1016\/0167-6423(95)00007-0_BIB33","series-title":"Proc. ACM Symp. on Functional Programming and Computer Architecture","first-page":"319","article-title":"Practical polymorphism","author":"Nikhil","year":"1985"},{"key":"10.1016\/0167-6423(95)00007-0_BIB34","series-title":"Equational reasoning","author":"Nipkow","year":"1992"},{"key":"10.1016\/0167-6423(95)00007-0_BIB35","series-title":"Proc. IEEE Symp. on Logic in Computer Science","article-title":"Functional unification of higher-order patterns","author":"Nipkow","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB36","series-title":"Proc. ACM Symp. on Principles of Programming Languages","article-title":"Type checking type classes","author":"Nipkow","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB37","series-title":"Proc. ACM Symp. on Functional Programming and Computer Architecture","first-page":"1","article-title":"Type classes and overloading resolution via order-sorted unification","volume":"Vol. 523","author":"Nipkow","year":"1991"},{"key":"10.1016\/0167-6423(95)00007-0_BIB38","unstructured":"J. Ophel and D. Duggan, Multi-parameter parametric overloading, Submitted."},{"key":"10.1016\/0167-6423(95)00007-0_BIB39","unstructured":"J. Ousterhout, TCL: An embeddable command language, in: Proc. USENIX Conf. (19990) 133\u2013146."},{"key":"10.1016\/0167-6423(95)00007-0_BIB40","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","article-title":"Linear unification","volume":"16","author":"Paterson","year":"1978","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/0167-6423(95)00007-0_BIB41","series-title":"Joint Framework for Information Technology (JFIT) Technical Conf.","first-page":"249","article-title":"The Glasgow Haskell compiler: A technical overview","author":"Peyton-Jones","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB42","series-title":"Proc. ACM Symp. on Principles of Programming Languages","first-page":"71","article-title":"Imperative functional programming","author":"Peyton-Jones","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB43","series-title":"Proc. ACM Symp. on Lisp and Functional Programming","first-page":"153","article-title":"Partial polymorphic type inference and higher-order unification","author":"Pfenning","year":"1988"},{"key":"10.1016\/0167-6423(95)00007-0_BIB44","series-title":"Proc. Coll. on Trees in Algebra and Programming","first-page":"391","article-title":"Linear unification of higher-order patterns","volume":"vol. 668","author":"Qian","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB45","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/0167-6423(95)00007-0_BIB46","series-title":"Functional Programming, Workshops in Computing","first-page":"249","article-title":"Time profiling a lazy functional compiler","author":"Sansom","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB47","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF01178581","article-title":"The calculus of context relations","volume":"28","author":"Snelting","year":"1991","journal-title":"Acta Inform."},{"key":"10.1016\/0167-6423(95)00007-0_BIB48","article-title":"An explanation-based polymorphic type checker for Standard ML","author":"Soosaipillai","year":"1990"},{"key":"10.1016\/0167-6423(95)00007-0_BIB49","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth first search and linear graph algorithms","volume":"1","author":"Tarjan","year":"1972","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0167-6423(95)00007-0_BIB50","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/321879.321884","article-title":"Efficiency of a good but not linear set union algorithm","volume":"22","author":"Tarjan","year":"1975","journal-title":"J. ACM"},{"key":"10.1016\/0167-6423(95)00007-0_BIB51","article-title":"Description, implementation and practical comparison of unification algorithms","author":"Trum","year":"1978"},{"key":"10.1016\/0167-6423(95)00007-0_BIB52","series-title":"Proc. ACM Symp. on Functional Programming and Computer Architecture","first-page":"1","article-title":"Miranda: A nonstrict functional language with polymorphic types","volume":"Vol. 201","author":"Turner","year":"1985"},{"key":"10.1016\/0167-6423(95)00007-0_BIB53","article-title":"Interactively testing remote servers using the Python programming language","author":"van Rossum","year":"1993"},{"key":"10.1016\/0167-6423(95)00007-0_BIB54","article-title":"Extending attribute grammar and type inference algorithms","author":"Walz","year":"1989"},{"key":"10.1016\/0167-6423(95)00007-0_BIB55","series-title":"Proc. ACM Symp. on Principles of Programming Languages","first-page":"38","article-title":"Finding the source of type errors","author":"Wand","year":"1986"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642395000070?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642395000070?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T05:29:10Z","timestamp":1555392550000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0167642395000070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,7]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,7]]}},"alternative-id":["0167642395000070"],"URL":"https:\/\/doi.org\/10.1016\/0167-6423(95)00007-0","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[1996,7]]}}}