{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:18:15Z","timestamp":1742617095285,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540156482"},{"type":"electronic","value":"9783540395270"}],"license":[{"start":{"date-parts":[[1985,1,1]],"date-time":"1985-01-01T00:00:00Z","timestamp":473385600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_18","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:20:23Z","timestamp":1330194023000},"page":"225-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Second-order logical relations"],"prefix":"10.1007","author":[{"given":"John C.","family":"Mitchell","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":"18_CR1","unstructured":"Barendregt, H.P, The Lambda Calculus: Its Syntax and Semantics. North Holland 1981."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Bruce, K. and Meyer, A., A Completeness Theorem for Second-Order Polymorphic Lambda Calculus. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), 1984, pages 131\u2013144..","DOI":"10.1007\/3-540-13346-1_6"},{"key":"18_CR3","unstructured":"Bruce, K.B., Meyer, A.R. and Mitchell, J.C., The semantics of second-order lambda calculus. to appear"},{"key":"18_CR4","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1137\/0208044","volume":"8","author":"J. Donahue","year":"1979","unstructured":"Donahue, J., On the semantics of data type. SIAM J. Computing 8 1979, pages 546\u2013560","journal-title":"SIAM J. Computing"},{"issue":"1","key":"18_CR5","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. pages 151\u2013185","journal-title":"JACM"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Friedman, H., Equality Between Functionals. In R. Parikh (ed.), Logic Colloquium, pages 22\u201337. Springer-Verlag 1975.","DOI":"10.1007\/BFb0064870"},{"key":"18_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 Fenstad, J.E. (ed.), 2 nd Scandinavian Logic Symp., pages 63\u201392. North-Holland 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Haynes, C.T., A Theory of Data Type Representation Independence. In Int. Symp. on Semantics of Data Types, Springer-Verlag, 1984, pages 157\u2013176.","DOI":"10.1007\/3-540-13346-1_8"},{"issue":"2","key":"18_CR9","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Henkin, L., Completeness in the Theory of Types. Journal of Symbolic Logic 15, 2 June 1950. pages 81\u201391","journal-title":"Journal of Symbolic Logic"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Leivant, D., Polymorphic Type Inference. In Proc. 10-th ACM Symp. on Principles of Programming Languages, 1983, pages 88\u201398.","DOI":"10.1145\/567067.567077"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"MacQueen, D., Plotkin, G and Sethi, R., An Ideal Model for Polymorphic Types. In Proc. 11-th ACM Symp. on Principles of Prog. Lang, January, 1984, pages 165\u2013174.","DOI":"10.1145\/800017.800528"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"MacQueen, D. and Sethi, R., A Semantic Model of Types for Applicative Languages. In ACM Symp. on Lisp and Functional Programming, 1982, pages 243\u2013252..","DOI":"10.1145\/800068.802156"},{"key":"18_CR13","unstructured":"McCracken, N., An Investigation of a Programming Language with a Polymorphic Type Structure. Syracuse Univ. 1979."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"McCracken, N., The Typechecking of Programs with Implicit Type Structure. In Proc. Int'l Symp. on Semantics of Data Types, June, 1984, pages 301\u2013316.","DOI":"10.1007\/3-540-13346-1_15"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Type Inference and Type Containment. In Proc. Int'l Symp. on Semantics of Data Types, June, 1984, pages 257\u2013278.","DOI":"10.1007\/3-540-13346-1_13"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Semantic models for second-order lambda calculus. In Proc. 25-th IEEE Symp. on Foundations of Computer Science, 1984, pages 289\u2013299.","DOI":"10.1109\/SFCS.1984.715927"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C. and Plotkin, G.D., Abstract types have existential types. In Proc. 12-th ACM Symp. on Principles of Programming Languages, January, 1985. pp. 37\u201351.","DOI":"10.1145\/318593.318606"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Mulmuley, K., A semantic characterization of full abstraction for typed lambda calculus. In Proc. 25-th IEEE Symp. on Foundations of Computer Science, 1984, pages 279\u2013288.","DOI":"10.1109\/SFCS.1984.715926"},{"key":"18_CR19","unstructured":"Plotkin, G.D., Lambda definability in the full type hierarchy. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363\u2013373. Academic Press 1980."},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C., Towards a Theory of Type Structure. In Paris Colloq. on Programming, Springer-Verlag, 1974, pages 408\u2013425.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"18_CR21","unstructured":"Reynolds, J.C., Types, Abstraction, and Parametric Polymorphism. In IFIP Congress, 1983."},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C., Polymorphism is not Set-Theoretic. In Int. Symp. on Semantics of Data Types, Springer-Verlag, 1984, pages 145\u2013156.","DOI":"10.1007\/3-540-13346-1_7"},{"key":"18_CR23","unstructured":"Statman, R., Logical relations and the typed lambda calculus. (Manuscript.) To appear in Information and Control."},{"key":"18_CR24","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W., Intensional interpretation of functionals of finite type. J. Symbolic Logic 32 1967. pages 198\u2013212","journal-title":"J. Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:22:11Z","timestamp":1742588531000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_18"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1985]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}