{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T13:09:21Z","timestamp":1744290561119},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540489375"},{"type":"electronic","value":"9783540489382"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11924661_5","type":"book-chapter","created":{"date-parts":[[2006,10,27]],"date-time":"2006-10-27T13:42:39Z","timestamp":1161956559000},"page":"79-96","source":"Crossref","is-referenced-by-count":22,"title":["Relational Reasoning for Recursive Types and References"],"prefix":"10.1007","author":[{"given":"Nina","family":"Bohr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems","author":"A. Ahmed","year":"2006","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 69\u201383. Springer, Heidelberg (2006)"},{"key":"5_CR2","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":"5_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1006\/inco.1999.2828","volume":"155","author":"L. Birkedal","year":"1999","unstructured":"Birkedal, L., Harper, R.: Constructing interpretations of recursive types in an operational setting. Information and Computation\u00a0155, 3\u201363 (1999)","journal-title":"Information and Computation"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11693024_11","volume-title":"Programming Languages and Systems","author":"V. Koutavas","year":"2006","unstructured":"Koutavas, V., Wand, M.: Bisimulations for untyped imperative objects. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 146\u2013161. Springer, Heidelberg (2006)"},{"key":"5_CR5","first-page":"141","volume-title":"POPL 2006: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"V. Koutavas","year":"2006","unstructured":"Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: POPL 2006: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 141\u2013152. ACM Press, New York (2006)"},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1006\/inco.1996.0061","volume":"128","author":"I.A. Mason","year":"1996","unstructured":"Mason, I.A., Smith, S., Talcott, C.L.: From operational semantics to domain theory. Information and Computation\u00a0128(1), 26\u201347 (1996)","journal-title":"Information and Computation"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A. Pitts","year":"1996","unstructured":"Pitts, A.: Relational properties of domains. Information and Computation\u00a0127, 66\u201390 (1996)","journal-title":"Information and Computation"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/3-540-57182-5_8","volume-title":"Mathematical Foundations of Computer Science 1993","author":"A.M. Pitts","year":"1993","unstructured":"Pitts, A.M., Stark, I.: Observable properties of higher order functions that dynamically create local names, or: What\u2019s new? In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol.\u00a0711, pp. 122\u2013141. Springer, Heidelberg (1993)"},{"issue":"1-3","key":"5_CR9","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.scico.2004.01.007","volume":"50","author":"U. Reddy","year":"2004","unstructured":"Reddy, U., Yang, H.: Correctness of data representations involving heap data structures. Science of Computer Programming\u00a050(1-3), 129\u2013160 (2004)","journal-title":"Science of Computer Programming"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002)","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, pp. 55\u201374. IEEE Press, Los Alamitos (2002)"},{"key":"5_CR11","unstructured":"Shinwell, M.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, Computer Laboratory, Cambridge (December 2004)"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.tcs.2005.06.003","volume":"342","author":"M.R. Shinwell","year":"2005","unstructured":"Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theoretical Computer Science\u00a0342, 28\u201355 (2005)","journal-title":"Theoretical Computer Science"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. In: ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL), Long Beach, California (2005)","DOI":"10.1145\/1040305.1040311"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11924661_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:45:12Z","timestamp":1619509512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11924661_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540489375","9783540489382"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11924661_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}