{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:18:11Z","timestamp":1742617091783,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"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_6","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:05:14Z","timestamp":1330193114000},"page":"131-144","source":"Crossref","is-referenced-by-count":16,"title":["The semantics of second order polymorphic lambda calculus"],"prefix":"10.1007","author":[{"given":"Kim B.","family":"Bruce","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert R.","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"1091","DOI":"10.1016\/S0049-237X(08)71129-7","volume-title":"Handbook of Mathematical Logic","author":"H.P. Barendregt","year":"1977","unstructured":"Barendregt, H.P. (1977). \"The Type free lambda calculus,\" Handbook of Mathematical Logic, J. Barwise, ed., North Holland, New York, 1091\u20131132."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Barendregt, H., Coppo, M., and Dezani-Ciancaglini, M. (1982). \"A filter lambda model and the completeness of type assignment,\" preprint.","DOI":"10.2307\/2273659"},{"key":"6_CR3","unstructured":"Berry, G. (1980). \"On the definition of lambda-calculus models,\" INRIA Rapports de Recherche, No. 46, 12 pp."},{"key":"6_CR4","unstructured":"Bruce, K., and G. Longo. (1984). \"An elementary approach to the solution of recursive domain equations,\" preprint."},{"key":"6_CR5","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1137\/0208044","volume":"8","author":"J. Donahue","year":"1979","unstructured":"Donahue, James (1979). \"On the semantics of \"data type,\" SIAM J. Computing 8, 546\u2013560.","journal-title":"SIAM J. Computing"},{"key":"6_CR6","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S. Fortune","year":"1983","unstructured":"Fortune, S., D. Leivant, and M. O'Donnell (1983). \"The expressiveness of simple and second-order type structures,\" JACM, 30, 151\u2013185.","journal-title":"JACM"},{"key":"6_CR7","unstructured":"Girard, J.-Y. (1972). \"Interpretation fonctionelle et elimination des coupures dans l'arithemetique d'order superieur,\" Ph.D. Dissertation, Paris."},{"key":"6_CR8","volume-title":"A Theory of data type representation independence","author":"C. Haynes","year":"1982","unstructured":"Haynes, C. (1982). \"A Theory of data type representation independence,\" Ph.D. Dissertation, University of Iowa, Iowa City, Iowa."},{"key":"6_CR9","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19800261902","volume":"26","author":"R. Hindley","year":"1980","unstructured":"Hindley, R., and G. Longo (1980). \"Lambda-calculus models and extensionality,\" Zeit. f. Math. Logik u. Grund. der Math. 26, 289\u2013310.","journal-title":"Zeit. f. Math. Logik u. Grund. der Math."},{"key":"6_CR10","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1016\/S0019-9958(82)90796-3","volume":"52","author":"K. Koymans","year":"1982","unstructured":"Koymans, K. (1982). \"Models of the \u03b3-calculus,\" Information and Control, 52, 306\u2013332.","journal-title":"Information and Control"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Leivant, D. (1983a). \"Polymorphic Type Inference,\" POPL Proceedings, pp. 88\u201398.","DOI":"10.1145\/567067.567077"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"__________(1983b). \"Structural Semantics for Polymorphic Data Types,\" POPL Proceedings, pp. 155\u2013166.","DOI":"10.1145\/567067.567083"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"MacQueen, D., and Sethi, R. (1982). \"A semantic model of types for applicative languages,\" preprint.","DOI":"10.1145\/800068.802156"},{"key":"6_CR14","unstructured":"McCracken, N.J. (1979). \"An investigation of a programming language with a polymorphic type structure,\" Ph.D. dissertation, Syracuse University."},{"key":"6_CR15","unstructured":"__________(1984). \"A finitary retract model for the polymorphic lambda-calculus,\" to appear, Information and Control."},{"key":"6_CR16","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"12","author":"A. Meyer","year":"1982","unstructured":"Meyer, A. (1982). \"What is a model of \u03b3-calculus?\", Information and Control, 12, 87\u2013122.","journal-title":"Information and Control"},{"key":"6_CR17","first-page":"348","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R. (1978). \"A theory of type polymorphism in programming,\" JCSS 17, pp. 348\u2013375.","journal-title":"JCSS"},{"key":"6_CR18","unstructured":"Mitchell, J. (1984). Personal communication."},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C. (1974). \"Towards a theory of type structure,\" Colloquium on Programming, Paris.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"6_CR20","unstructured":"__________(1983). \"Types, abstraction, and parametric polymorphism,\" preprint of paper delivered at IFIP Congress '83, 11 pp."},{"key":"6_CR21","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","volume":"5","author":"D.S. Scott","year":"1976","unstructured":"Scott, D.S. (1976). \"Data types as lattices,\" SIAM J. on Computing, 5, 522\u2013587.","journal-title":"SIAM J. on Computing"},{"key":"6_CR22","series-title":"Studies on Logic","first-page":"381","volume-title":"The Kleene Symposium","author":"D.S. Scott","year":"1980","unstructured":"\u2014 (1980a). \"Lambda calculus: some models, some philosophy,\" The Kleene Symposium, Barwise et. al, ed., Studies on Logic 101, North Holland, New York, 381\u2013421."},{"key":"6_CR23","volume-title":"A space of retracts","author":"D.S. Scott","year":"1980","unstructured":"\u2014 (1980b). \"A space of retracts,\" manuscript, Merton College, Oxford."},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Statman, R. (1981). \"Number theoretic functions computable by polymophic programs,\" in Twenty-Second Annual Symposium on Foundations of Computer Science, 279\u2013282.","DOI":"10.1109\/SFCS.1981.24"}],"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_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:19:56Z","timestamp":1742588396000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-13346-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9783540133469","9783540388913"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-13346-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1984]]}}}