{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:19:39Z","timestamp":1770297579110,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642005954","type":"print"},{"value":"9783642005961","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00596-1_32","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T01:13:03Z","timestamp":1238116383000},"page":"456-470","source":"Crossref","is-referenced-by-count":16,"title":["Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types"],"prefix":"10.1007","author":[{"given":"Lars","family":"Birkedal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristian","family":"St\u00f8vring","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob","family":"Thamsborg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Plotkin, G.D.: A per model of polymorphism and recursive types. In: Proceedings of LICS, pp. 355\u2013365 (1990)","DOI":"10.1109\/LICS.1990.113761"},{"key":"32_CR2","unstructured":"Ahmed, A.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of POPL (to appear, 2009)","DOI":"10.1145\/1594834.1480925"},{"issue":"1","key":"32_CR4","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90074-C","volume":"91","author":"R.M. Amadio","year":"1991","unstructured":"Amadio, R.M.: Recursion over realizability structures. Information and Computation\u00a091(1), 55\u201385 (1991)","journal-title":"Information and Computation"},{"key":"32_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983504","volume-title":"Domains and Lambda-Calculi","author":"R.M. Amadio","year":"1998","unstructured":"Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge University Press, Cambridge (1998)"},{"issue":"3","key":"32_CR6","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0022-0000(89)90027-5","volume":"39","author":"P. America","year":"1989","unstructured":"America, P., Rutten, J.J.M.M.: Solving reflexive domain equations in a category of complete metric spaces. J. Comput. Syst. Sci.\u00a039(3), 343\u2013375 (1989)","journal-title":"J. Comput. Syst. Sci."},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/11417170_8","volume-title":"Typed Lambda Calculi and Applications","author":"N. Benton","year":"2005","unstructured":"Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 86\u2013101. Springer, Heidelberg (2005)"},{"key":"32_CR8","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Relational parametricity for references and recursive types. In: Proceedings of TLDI (to appear, 2009)"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/11924661_5","volume-title":"Programming Languages and Systems","author":"N. Bohr","year":"2006","unstructured":"Bohr, N., Birkedal, L.: Relational reasoning for recursive types and references. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 79\u201396. Springer, Heidelberg (2006)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/BFb0035759","volume-title":"Automata, Languages and Programming","author":"F. Cardone","year":"1989","unstructured":"Cardone, F.: Relational semantics for recursive types and bounded quantification. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 164\u2013178. Springer, Heidelberg (1989)"},{"key":"32_CR11","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/j.entcs.2007.02.010","volume":"172","author":"K. Crary","year":"2007","unstructured":"Crary, K., Harper, R.: Syntactic logical relations for polymorphic and recursive types. Electronic Notes in Theoretical Computer Science\u00a0172, 259\u2013299 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"4","key":"32_CR12","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10990-006-0480-6","volume":"19","author":"P.B. Levy","year":"2006","unstructured":"Levy, P.B.: Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation\u00a019(4), 377\u2013414 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"1\/2","key":"32_CR13","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0019-9958(86)80019-5","volume":"71","author":"D.B. MacQueen","year":"1986","unstructured":"MacQueen, D.B., Plotkin, G.D., Sethi, R.: An ideal model for recursive polymorphic types. Information and Control\u00a071(1\/2), 95\u2013130 (1986)","journal-title":"Information and Control"},{"key":"32_CR14","volume-title":"Foundations for Programming Languages","author":"J.C. Mitchell","year":"1996","unstructured":"Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)"},{"key":"32_CR15","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093, 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78739-6_26","volume-title":"Programming Languages and Systems","author":"R.L. Petersen","year":"2008","unstructured":"Petersen, R.L., Birkedal, L., Nanevski, A., Morrisett, G.: A realizability model for impredicative hoare type theory. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 337\u2013352. Springer, Heidelberg (2008)"},{"key":"32_CR17","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"32_CR18","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A.M. Pitts","year":"1996","unstructured":"Pitts, A.M.: Relational properties of domains. Information and Computation\u00a0127, 66\u201390 (1996)","journal-title":"Information and Computation"},{"key":"32_CR19","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.entcs.2004.08.008","volume":"73","author":"G.D. Plotkin","year":"2004","unstructured":"Plotkin, G.D., Power, J.: Computational effects and operations: An overview. Electronic Notes in Theoretical Computer Science\u00a073, 149\u2013163 (2004)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1-2","key":"32_CR20","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/S0304-3975(96)80711-0","volume":"170","author":"J.J.M.M. Rutten","year":"1996","unstructured":"Rutten, J.J.M.M.: Elements of generalized ultrametric domain theory. Theoretical Computer Science\u00a0170(1-2), 349\u2013381 (1996)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"32_CR21","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1137\/0211062","volume":"11","author":"M.B. Smyth","year":"1982","unstructured":"Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM Journal on Computing\u00a011(4), 761\u2013783 (1982)","journal-title":"SIAM Journal on Computing"},{"key":"32_CR22","unstructured":"Wagner, K.R.: Solving Recursive Domain Equations with Enriched Categories. PhD thesis, Carnegie Mellon University (1994)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00596-1_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,7]],"date-time":"2019-03-07T07:23:25Z","timestamp":1551943405000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00596-1_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005954","9783642005961"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00596-1_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}