{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:59:54Z","timestamp":1725663594377},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_38","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:45:51Z","timestamp":1330209951000},"page":"1-17","source":"Crossref","is-referenced-by-count":2,"title":["A semantics for type checking"],"prefix":"10.1007","author":[{"given":"Gordon","family":"Plotkin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"1_CR1","volume-title":"The lambda calculus: its syntax and semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P. The lambda calculus: its syntax and semantics. Amsterdam: North-Holland (1984)."},{"issue":"4","key":"1_CR2","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P., Coppo M., and Dezani-Ciancaglini, M. A filter lambda model and the completeness of type assignment. J. Symbolic Logic\n48\/4, pp. 931\u2013940 (1984).","journal-title":"J. Symbolic Logic"},{"key":"1_CR3","first-page":"241","volume-title":"Logic Colloquium '82","author":"M. Coppo","year":"1983","unstructured":"Coppo, M., Dezani, M., Honsell F. and Longo, G. Extended type structures and filter lambda models, in Logic Colloquium '82, ed. G. Lolli et al, pp 241\u2013262. Amsterdam: North Holland (1983)"},{"key":"1_CR4","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/LICS.1988.5101","volume-title":"Proc. of the Third Annual IEEE Symposium on Logic in Computer Science","author":"P. Giannini","year":"1988","unstructured":"Giannini, P. and Ronchi Della Rocca, S. Characterisations of typings in polymorphic type discipline. In Proc. of the Third Annual IEEE Symposium on Logic in Computer Science, pp. 61\u201371. Los Alamitos: Computer Society Press of the IEEE (1988)."},{"key":"1_CR5","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. Theoret. Comput. Sci.\n22, pp. 1\u201317 (1983).","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR6","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. Theoret. Comput. Sci.\n22, pp. 127\u2013133 (1983).","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR7","unstructured":"Jay, C. B. Long \u03b2\u03b7-normal forms in confluent categories. To appear (1991)."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Leivant, D. Polymorphic type inference, in Proceedings, 10th Annual ACM Symposium on Principles of Programming Languages, pp. 88\u201389 (1983).","DOI":"10.1145\/567067.567077"},{"key":"1_CR9","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1985","unstructured":"Milner, R. A theory of type polymorphism in programming. J. Comput. System Sci.\n17, pp. 348\u2013375 (1985).","journal-title":"J. Comput. System Sci."},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","volume":"76","author":"J. C. Mitchell","year":"1988","unstructured":"Mitchell, J. C. Polymorphic type inference and containment. Information and Computation\n76, pp. 211\u2013249 (1988).","journal-title":"Information and Computation"},{"key":"1_CR11","unstructured":"Plotkin, G.D. A set-theoretical definition of application. Research Memorandum MIP-R-95, 32 pp. Dept. of Machine Intelligence and Perception, University of Edinburgh (1972)."},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-18508-9_23","volume-title":"Category theory and Computer Science","author":"D.E. Rydeheard","year":"1987","unstructured":"Rydeheard, D.E. and Stell, J.G. Foundations of equational deduction: a categorical treatment of equational proofs and unification algorithms, in: Pitt et al, (eds), Category theory and Computer Science, Lecture Notes in Computer Science\n283 pp. 114\u2013139. Berlin: Springer Verlag (1987)."},{"key":"1_CR13","first-page":"65","volume-title":"Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science","author":"R.A.G. Seely","year":"1987","unstructured":"Seely, R.A.G. Modelling computations a 2-categorical framework, in: Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, pp. 65\u201371. Los Alamitos: Computer Society Press of the IEEE (1987)."},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BFb0029599","volume-title":"Proceedings, Mathematical Foundations of Computer Science","author":"J. Tiuryn","year":"1990","unstructured":"Tiuryn, J. Type inference problems: a survey, in B. Rovan (ed.) Proceedings, Mathematical Foundations of Computer Science. Lecture Notes in Computer Science\n452 pp. 105\u2013120. Berlin: Springer Verlag (1990)."},{"key":"1_CR15","unstructured":"Yokouchi, H. Embedding second order type system into intersection type system and its application to type inference. To appear (1991)."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:21:25Z","timestamp":1619572885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}