{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:48:51Z","timestamp":1725662931131},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540133469"},{"type":"electronic","value":"9783540388913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1984]]},"DOI":"10.1007\/3-540-13346-1_13","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:04:38Z","timestamp":1330175078000},"page":"257-277","source":"Crossref","is-referenced-by-count":8,"title":["Type inference and type containment"],"prefix":"10.1007","author":[{"given":"John","family":"Mitchell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"4","key":"13_CR1","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M. and Dezani-Ciancaglini, M. A Filter Lambda Model and the Completeness of Type Assignment. J. Symbolic Logic 48, 4 (1983). pp 931\u2013940.","journal-title":"J. Symbolic Logic"},{"key":"13_CR2","unstructured":"Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1981."},{"key":"13_CR3","unstructured":"Bruce, K. and Meyer, A. A Completeness Theorem for Second-Order Polymorphic Lambda Calculus. These proceedings."},{"key":"13_CR4","unstructured":"Curry, H.B and Feys, R. Combinatory Logic I. North-Holland, 1958."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Damas, L. and Milner, R. Principal Type Schemes for Functional Programs. 9-th ACM Symposium on Principles of Programming Languages, 1982, pp. 207\u2013212.","DOI":"10.1145\/582153.582176"},{"issue":"1","key":"13_CR6","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S. Fortune","year":"1983","unstructured":"Fortune, S., Leivant, D. and O'Donnel, M. The Expressiveness of Simple and Second Order Type Structures. JACM 30, 1 (1983). pp 151\u2013185","journal-title":"JACM"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y. Une extension de l'interpretation de G\u00f6del \u00e0 l'analyse, et son application \u00e0 l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types. In 2 nd Scandinavian Logic Symp., Fenstad, J.E., Ed., North-Holland, 1971, pp. 63\u201392.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"13_CR8","unstructured":"Haynes, C.T. A Theory of Data Type Representation Independence. Ph.D. Th., Univ. of Iowa, Dept. of Computer Science, 1982. Technical Report 82-04."},{"key":"13_CR9","first-page":"29","volume":"146","author":"R. Hindley","year":"1969","unstructured":"Hindley, R. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. AMS 146 (1969). pp 29\u201360.","journal-title":"Trans. AMS"},{"key":"13_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(83)90136-6","volume":"22","author":"R. Hindley","year":"1983","unstructured":"Hindley, R. The Completeness Theorem for Typing Lambda Terms. Theor. Comp. Sci. 22 (1983). pp 1\u201317.","journal-title":"Theor. Comp. Sci."},{"key":"13_CR11","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0304-3975(83)90141-X","volume":"22","author":"R. Hindley","year":"1983","unstructured":"Hindley, R. Curry's Type Rules Are Complete with Respect to the F-Semantics Too. Theor. Comp. Sci. 22 (1983). pp 127\u2013133.","journal-title":"Theor. Comp. Sci."},{"key":"13_CR12","unstructured":"Howard, W. The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, Seldin, J.P. and J.R. Hindley, Eds., Academic Press, 1980, pp. 479\u2013490."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Leivant, D. Polymorphic Type Inference. Proc. 10-th ACM Symp. on Principles of Programming Languages, 1983, pp. 88\u201398.","DOI":"10.1145\/567067.567077"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Leivant, D. Structural Semantics for Polymorphic Types. Proc. 10-th ACM Symp. on Principles of Programming Languages, 1983, pp. 155\u2013166.","DOI":"10.1145\/567067.567083"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"MacQueen, D. and Sethi, R. A Semantic Model of Types for Applicative Languages. ACM Symp. on LISP and Functional Programming, 1982, pp. 243\u2013252.","DOI":"10.1145\/800068.802156"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"MacQueen, D., Plotkin, G and Sethi, R. An Ideal Model for Polymorphic Types. Proc. 11-th ACM Symp. on Principles of Prog. Lang., January, 1984, pp. 165\u2013174.","DOI":"10.1145\/800017.800528"},{"key":"13_CR17","unstructured":"McCracken, N. An Investigation of a Programming Language with a Polymorphic Type Structure. Ph.D. Th., Syracuse Univ., 1979."},{"issue":"1","key":"13_CR18","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A.R. Meyer","year":"1982","unstructured":"Meyer, A.R. What Is A Model of the Lambda Calculus?. Information and Control 52, 1 (1982). pp 87\u2013122.","journal-title":"Information and Control"},{"key":"13_CR19","first-page":"348","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R. A Theory of Type Polymorphism in Programming. JCSS 17 (1978). pp 348\u2013375.","journal-title":"JCSS"},{"key":"13_CR20","unstructured":"Mitchell, J.C. Combinatory Models of Polymorphic Lambda Calculus. Manuscript (1984)."},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C. Coercion and Type Inference (Summary). Proc. 11-th ACM Symp. on Principles of Programming Languages, January, 1984, pp. 175\u2013185.","DOI":"10.1145\/800017.800529"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C. Towards a Theory of Type Structure. Paris Colloq. on Programming, 1974, pp. 408\u2013425.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Wand, M. A Types-as-Sets Semantics for Milner-Style Polymorphism. Proc. 11-th ACM Symp. on Principles of Programming Languages, January, 1984, pp. 158\u2013164.","DOI":"10.1145\/800017.800527"}],"container-title":["Lecture Notes in Computer Science","Semantics of Data Types"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-13346-1_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:07:22Z","timestamp":1605625642000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-13346-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9783540133469","9783540388913"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-13346-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1984]]}}}