{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:15:56Z","timestamp":1725488156064},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540419600"},{"type":"electronic","value":"9783540454137"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45413-6_24","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T08:51:43Z","timestamp":1186217503000},"page":"298-314","source":"Crossref","is-referenced-by-count":2,"title":["Second-Order Pre-logical Relations and Representation Independence"],"prefix":"10.1007","author":[{"given":"Hans","family":"Lei\u03b2","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,4,25]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/0890-5401(90)90044-I","volume":"85","author":"K. B. Bruce","year":"1990","unstructured":"Kim B. Bruce, Albert R. Meyer, and John C. Mitchell, The semantics of second-order lambda calculus, Information and Computation 85 (1990), 76\u2013134.","journal-title":"Information and Computation"},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1007\/3-540-48168-0_37","volume-title":"Proc. CSL\u201999","author":"J. Erskine Hannay","year":"1999","unstructured":"Jo Erskine Hannay, Specification refinement with system F, In Proc. CSL\u201999, LNCS 1683, Springer Verlag, 1999, pp. 530\u2013545."},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/3-540-44936-1","volume-title":"3rd Intl. Conf. on Foundations of Software Science and Computation Structures. European Joint Conferences on Theory and Practice of Software (ETAPS\u20192000)","author":"F. Honsell","year":"2000","unstructured":"Furio Honsell, John Longley, Donald Sannella, and Andrzej Tarlecki, Constructive data refinement in typed lambda calculus, 3rd Intl. Conf. on Foundations of Software Science and Computation Structures. European Joint Conferences on Theory and Practice of Software (ETAPS\u20192000), LNCS 1784, Springer Verlag, 2000, pp. 149\u2013164."},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/3-540-48168-0_38","volume-title":"Proc. Computer Science Logic, CSL\u201999","author":"F. Honsell","year":"1999","unstructured":"Furio Honsell and Donald Sannella, Pre-logical relations, Proc. Computer Science Logic, CSL\u201999, LNCS 1683, Springer Verlag, 1999, pp. 546\u2013561."},{"doi-asserted-by":"crossref","unstructured":"Xavier Leroy, Applicative functors and fully transparent higher-order modules, Proc. of the 22nd Annual ACM Symposium on Principles of Programming Languages, ACM, 1995, pp. 142\u2013153.","key":"24_CR5","DOI":"10.1145\/199448.199476"},{"doi-asserted-by":"crossref","unstructured":"John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM Symposium on Principles of Programming Languages, January 1986, pp. 263\u2013276.","key":"24_CR6","DOI":"10.1145\/512644.512669"},{"doi-asserted-by":"crossref","unstructured":"John C. Mitchell, On the equivalence of data representations, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honour of John C. McCarthy (V. Lifschitz, ed.), Academic Press, 1991, pp. 305\u2013330.","key":"24_CR7","DOI":"10.1016\/B978-0-12-450010-5.50023-2"},{"key":"24_CR8","volume-title":"Foundations for programming languages","author":"J. C. Mitchell","year":"1996","unstructured":"John C. Mitchell, Foundations for programming languages, The MIT Press, Cambridge, Mass., 1996."},{"key":"24_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-15648-8_18","volume-title":"Proc. Logics of Programs","author":"J. C. Mitchell","year":"1985","unstructured":"John C. Mitchell and Albert Meyer, Second-order logical relations, Proc. Logics of Programs, LNCS 193, Springer Verlag, 1985, pp. 225\u2013236."},{"doi-asserted-by":"crossref","unstructured":"John C. Mitchell and Gordon D. Plotkin, Abstract types have existential type, 12-th ACM Symposium on Principles of Programming Languages, 1985, pp. 37\u201351.","key":"24_CR10","DOI":"10.1145\/318593.318606"},{"key":"24_CR11","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The definition of Standard ML (revised)","author":"R. Milner","year":"1997","unstructured":"Robin Milner, Mads Tofte, Robert Harper, and David MacQueen, The definition of Standard ML (revised), The MIT Press, Cambridge, MA, 1997."},{"unstructured":"Gordon D. Plotkin, Lambda definability in the full type hierarchy, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 363\u2013373.","key":"24_CR12"},{"key":"24_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-45022-X_9","volume-title":"ICALP 2000","author":"G. Plotkin","year":"2000","unstructured":"Gordon Plotkin, John Power, Don Sannella, and Robert Tennent, Lax logical relations, ICALP 2000, Springer LNCS 1853, 2000, pp. 85\u2013102."},{"key":"24_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/3-540-44622-2_34","volume-title":"Proc. Computer Science Logic, CSL 2000","author":"J. Power","year":"2000","unstructured":"John Power and Edmund Robinson, Logical relations and data abstraction, Proc. Computer Science Logic, CSL 2000, LNCS 1862, Springer-Verlag, 2000, pp. 497\u2013511."},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"R. Statman, Logical relations and the typed lambda calculus, Information and Control 65 (1985), 85\u201397.","journal-title":"Information and Control"},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"W.W. Tait, Intensional interpretation of functionals of finite type, Journal of Symbolic Logic 32 (1967), 198\u2013212.","journal-title":"Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45413-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T22:55:00Z","timestamp":1550444100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45413-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540419600","9783540454137"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45413-6_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}