{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:56:19Z","timestamp":1760043379131},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540713142"},{"type":"electronic","value":"9783540713166"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-71316-6_29","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:58:28Z","timestamp":1184590708000},"page":"426-440","source":"Crossref","is-referenced-by-count":4,"title":["A Rewriting Semantics for Type Inference"],"prefix":"10.1007","author":[{"given":"George","family":"Kuan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"MacQueen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert Bruce","family":"Findler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Programming Language Implementation and Logic Programming","author":"A.W. Appel","year":"1991","unstructured":"Appel, A.W., MacQueen, D.B.: Standard ML of New Jersey. In: Ma\u0142uszy\u0144ski, J., Wirsing, M. (eds.) PLILP 1991. LNCS, vol.\u00a0528, pp. 1\u201313. Springer, Heidelberg (1991)"},{"issue":"1-4","key":"29_CR2","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/176454.176460","volume":"2","author":"M. Beaven","year":"1993","unstructured":"Beaven, M., Stansifer, R.: Explaining type errors in polymorphic languages. ACM Letters on Programming Languages and Systems\u00a02(1-4), 17\u201330 (1993)","journal-title":"ACM Letters on Programming Languages and Systems"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Bravenboer, M., et al.: Stratego\/XT Tutorial, Examples, and Reference Manual for Stratego\/XT 0.16. Department of Information and Computing Sciences, Universiteit Utrecht, Utrecht, The Netherlands (November 2005)","DOI":"10.1145\/1111542.1111558"},{"issue":"2","key":"29_CR4","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/0167-6423(87)90019-0","volume":"8","author":"L. Cardelli","year":"1987","unstructured":"Cardelli, L.: Basic polymorphic typechecking. Science of Computer Programming\u00a08(2), 147\u2013172 (1987)","journal-title":"Science of Computer Programming"},{"key":"29_CR5","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/263699.263744","volume-title":"POPL \u201997: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"P. Cousot","year":"1997","unstructured":"Cousot, P.: Types as abstract interpretations. In: POPL \u201997: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 316\u2013331. ACM Press, New York (1997)"},{"key":"29_CR6","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1111\/j.1746-8361.1969.tb01183.x","volume":"23","author":"H.B. Curry","year":"1969","unstructured":"Curry, H.B.: Modified basic functionality in combinatory logic. Dialectica\u00a023, 83\u201392 (1969)","journal-title":"Dialectica"},{"key":"29_CR7","unstructured":"Damas, L.: unpublished note (1982)"},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Technical Report BRICS RS-04-26, Department of Computer Science, University of Aarhus, Aarhus, Denmark (2004), http:\/\/citeseer.ist.psu.edu\/danvy04refocusing.html","DOI":"10.7146\/brics.v11i26.21851"},{"key":"29_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0167-6423(95)00007-0","volume":"27","author":"D. Duggan","year":"1996","unstructured":"Duggan, D., Bent, F.: Explaining type inference. Science of Computer Programming\u00a027, 37\u201383 (1996)","journal-title":"Science of Computer Programming"},{"key":"29_CR10","unstructured":"Felleisen, M., Flatt, M.: Programming languages and lambda calculi. Revision of 1989 edition (2003)"},{"issue":"2","key":"29_CR11","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M. Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: A revised report on the syntactic theories of sequential control and state. Theoretical Computer Science\u00a0103(2), 235\u2013271 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"1-3","key":"29_CR12","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/j.scico.2004.01.004","volume":"50","author":"C. Haack","year":"2004","unstructured":"Haack, C., Wells, J.B.: Type error slicing in implicitly typed higher-order languages. Sci. Comput. Program.\u00a050(1-3), 189\u2013224 (2004)","journal-title":"Sci. Comput. Program."},{"key":"29_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/944705.944707","volume-title":"ICFP \u201903: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming","author":"B. Heeren","year":"2003","unstructured":"Heeren, B., Hage, J., Swierstra, S.D.: Scripting the type inference process. In: ICFP \u201903: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pp. 3\u201313. ACM Press, New York (2003)"},{"key":"29_CR14","doi-asserted-by":"publisher","first-page":"29","DOI":"10.2307\/1995158","volume":"146","author":"J.R. Hindley","year":"1969","unstructured":"Hindley, J.R.: The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society\u00a0146, 29\u201340 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"29_CR15","unstructured":"Kahrs, S.: Polymorphic type checking by interpretation of code. Technical Report ECS-LFCS-92-238, University of Edinburgh (1992)"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Kuan, G.: A rewriting semantics for type inference. Technical Report TR-2007-01, University of Chicago (2007)","DOI":"10.1007\/978-3-540-71316-6_29"},{"issue":"4","key":"29_CR17","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1145\/291891.291892","volume":"20","author":"O. Lee","year":"1998","unstructured":"Lee, O., Yi, K.: Proofs about a folklore let-polymorphic type inference algorithm. ACM Transanctions on Programming Languages and Systems\u00a020(4), 707\u2013723 (1998)","journal-title":"ACM Transanctions on Programming Languages and Systems"},{"key":"29_CR18","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1159876.1159887","volume-title":"ML \u201906: Proceedings of the 2006 Workshop on ML","author":"B. Lerner","year":"2006","unstructured":"Lerner, B., Grossman, D., Chambers, C.: Seminal: searching for ML type-error messages. In: ML \u201906: Proceedings of the 2006 Workshop on ML, pp. 63\u201373. ACM Press, New York (2006)"},{"key":"29_CR19","unstructured":"Leroy, X.: Programmation du syst\u00e8me Unix en Caml Light. Technical report 147, INRIA (1992)"},{"issue":"2","key":"29_CR20","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst.\u00a04(2), 258\u2013282 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Matthews, J., et al.: A visual environment for developing context-sensitive term rewriting systems. In: Rewriting Techniques and Applications (2004)","DOI":"10.1007\/978-3-540-25979-4_21"},{"key":"29_CR22","unstructured":"McAdam, B.: How to repair type errors automatically. In: Trends in functional programming, pp. 87\u201398 (2002)"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"McAllester, D.: A logical algorithm for ML type inference. In: Rewriting Techniques and Applications (2003)","DOI":"10.1007\/3-540-44881-0_31"},{"key":"29_CR24","first-page":"348","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. JCSS\u00a017, 348\u2013375 (1978)","journal-title":"JCSS"},{"key":"29_CR25","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/944705.944708","volume-title":"ICFP \u201903: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming","author":"M. Neubauer","year":"2003","unstructured":"Neubauer, M., Thiemann, P.: Discriminative sum types locate the source of type errors. In: ICFP \u201903: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pp. 15\u201326. ACM Press, New York (2003)"},{"key":"29_CR26","unstructured":"Pa\u0161ali\u0107, E., Siek, J.G., Taha, W.: Concoqtion: Mixing indexed types and Hindley-Milner type inference. In: POPL \u201907: Conference record of the 34th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (2007)"},{"key":"29_CR27","unstructured":"R\u00e9my, D.: Extending ML type system with a sorted equational theory. Research Report 1766, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, Le Chesnay, France (1992)"},{"issue":"1","key":"29_CR28","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"29_CR29","unstructured":"Soosaipillai, H.: An explanation based polymorphic type checker for Standard ML. Master\u2019s Thesis (1990)"},{"key":"29_CR30","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/512644.512648","volume-title":"POPL \u201986: Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages","author":"M. Wand","year":"1986","unstructured":"Wand, M.: Finding the source of type errors. In: POPL \u201986: Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 38\u201343. ACM Press, New York (1986)"},{"key":"29_CR31","doi-asserted-by":"crossref","first-page":"115","DOI":"10.3233\/FI-1987-10202","volume":"10","author":"M. Wand","year":"1987","unstructured":"Wand, M.: A simple algorithm and proof for type inference. Fundamenta Infomaticae\u00a010, 115\u2013122 (1987)","journal-title":"Fundamenta Infomaticae"},{"key":"29_CR32","first-page":"59","volume-title":"SFP \u201999: Selected papers from the 1st Scottish Functional Programming Workshop (SFP99)","author":"J. Yang","year":"2000","unstructured":"Yang, J.: Explaining type errors by finding the source of a type conflict. In: SFP \u201999: Selected papers from the 1st Scottish Functional Programming Workshop (SFP99), Exeter, UK, pp. 59\u201367. Intellect Books, Oxford (2000)"},{"key":"29_CR33","unstructured":"Yang, J.: Improving Polymorphic Type Explanations. PhD thesis, Heriot-Watt University (2001)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71316-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T07:57:17Z","timestamp":1629359837000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71316-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540713142","9783540713166"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71316-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}