{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:11:15Z","timestamp":1767928275412,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540713883","type":"print"},{"value":"9783540713890","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71389-0_8","type":"book-chapter","created":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T16:22:53Z","timestamp":1183306973000},"page":"93-107","source":"Crossref","is-referenced-by-count":8,"title":["Relational Parametricity and Separation Logic"],"prefix":"10.1007","author":[{"given":"Lars","family":"Birkedal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Barnett, M., Naumann, D.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. In: Proc. of LICS\u201904 (2004)","DOI":"10.1109\/LICS.2004.1319626"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Benton, N.: Abstracting Allocation: The New new Thing. In: Proc. of CSL\u201906 (2006)","DOI":"10.1007\/11874683_12"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/11595014","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. 88\u2013101. Springer, Heidelberg (2005)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-540-31987-0_17","volume-title":"Programming Languages and Systems","author":"B. Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines and higher order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1017\/S0960129505004834","volume":"15","author":"L. Birkedal","year":"2005","unstructured":"Birkedal, L., M\u00f8gelberg, R.: Categorical models for Abadi-Plotkin\u2019s logic for parametricity. Mathematical Structures in Computer Science\u00a015, 709\u2013772 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: Proc. of POPL\u201904, Venice, Italy, pp. 220\u2013231 (2004)","DOI":"10.1145\/964001.964020"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: Proc. of LICS\u201905, pp. 260\u2013269 (2005)","DOI":"10.1109\/LICS.2005.47"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/978-3-540-30538-5_35","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"I. Mijajlovi\u0107","year":"2004","unstructured":"Mijajlovi\u0107, I., Torp-Smith, N., O\u2019Hearn, P.: Refinement and separation context. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 421\u2013433. Springer, Heidelberg (2004)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11575467_3","volume-title":"Programming Languages and Systems","author":"I. Mijajlovi\u0107","year":"2005","unstructured":"Mijajlovi\u0107, I., Yang, H.: Data refinements with low-level pointer operations. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 19\u201336. Springer, Heidelberg (2005)"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/331605.331611","volume":"47","author":"P. O\u2019Hearn","year":"2000","unstructured":"O\u2019Hearn, P., Reynolds, J.: From Algol to polymorphic linear lambda-calculus. Journal of the ACM\u00a047(1), 167\u2013223 (2000)","journal-title":"Journal of the ACM"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Science Logic","author":"H. Yang","year":"2001","unstructured":"Yang, H., O\u2019Hearn, P.W., Reynolds, J.C.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, Springer, Heidelberg (2001)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proc. of POPL\u201904, Venice, Italy, pp. 268\u2013280 (2004)","DOI":"10.1145\/982962.964024"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proc. of POPL\u201905, Long Beach, CA, USA, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Typed Lambda Calculi and Applications","author":"G. Plotkin","year":"1993","unstructured":"Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 361\u2013375. Springer, Heidelberg (1993)"},{"key":"8_CR15","first-page":"513","volume":"83","author":"J. Reynolds","year":"1983","unstructured":"Reynolds, J.: Types, abstraction, and parametric polymorphism. Information Processing\u00a083, 513\u2013523 (1983)","journal-title":"Information Processing"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of LICS\u201902, Copenhagen, Denmark, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"8_CR17","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":"8_CR18","unstructured":"Torp-Smith, N.: Advances in Separation Logic \u2014 A Study of Logics for Reasoning about Stateful Programs. PhD thesis, IT University of Copenhagen (2005)"},{"key":"8_CR19","unstructured":"Yang, H.: Relational separation logic. Theoretical Comput. Sci. (to appear, 2005)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71389-0_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:19:41Z","timestamp":1605745181000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71389-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540713883","9783540713890"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71389-0_8","relation":{},"subject":[]}}