{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:13:15Z","timestamp":1754485995960,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255932"},{"type":"electronic","value":"9783540320142"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11417170_8","type":"book-chapter","created":{"date-parts":[[2010,12,16]],"date-time":"2010-12-16T19:29:35Z","timestamp":1292527775000},"page":"86-101","source":"Crossref","is-referenced-by-count":47,"title":["Relational Reasoning in a Nominal Semantics for Storage"],"prefix":"10.1007","author":[{"given":"Nick","family":"Benton","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Leperchey","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Benton, N., Kennedy, A.: Monads, effects and transformations. In: 3rd International Workshop on Higher Order Operational Techniques in Semantics (HOOTS). Electronic Notes in Theoretical Computer Science, vol.\u00a026. Elsevier, Amsterdam (1999)","DOI":"10.1016\/S1571-0661(05)80280-4"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. Technical report, Microsoft Research (February 2005)","DOI":"10.1007\/11417170_8"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-45793-3_16","volume-title":"Computer Science Logic","author":"P.B. Levy","year":"2002","unstructured":"Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, p. 232. Springer, Heidelberg (2002)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Sieber, K.: Towards a fully abstract semantics for local variables: Preliminary report. In: Proceedings of the 15th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (January 1988)","DOI":"10.1145\/73560.73577"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/331605.331611","volume":"47","author":"P.W. O\u2019Hearn","year":"2000","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C.: From Algol to polymorphic linear lambda-calculus. Journal of the ACM\u00a047(1), 167\u2013223 (2000)","journal-title":"Journal of the ACM"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, p. 1. Springer, Heidelberg (2001)"},{"issue":"3","key":"8_CR7","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1145\/210346.210425","volume":"42","author":"P.W. O\u2019Hearn","year":"1995","unstructured":"O\u2019Hearn, P.W., Tennent, R.D.: Parametricity and local variables. Journal of the ACM\u00a042(3), 658\u2013709 (1995)","journal-title":"Journal of the ACM"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Tennent, R.D. (eds.): Progress in Theoretical Computer Science, Algol-like Languages. Birkh\u00e4user, Basel (1997) (Two volumes)","DOI":"10.1007\/978-1-4757-3851-3"},{"key":"8_CR9","unstructured":"Oles, F.J.: A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University (1982)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: [8], (1997)","DOI":"10.1007\/978-1-4757-3851-3_7"},{"key":"8_CR11","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.D.B.: 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)"},{"key":"8_CR12","series-title":"Publications of the Newton Institute","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics","author":"A.M. Pitts","year":"1998","unstructured":"Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics. Publications of the Newton Institute, pp. 227\u2013273. Cambridge University Press, Cambridge (1998)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Relational properties of domains. Information and Computation\u00a0127(2) (1996)","DOI":"10.1006\/inco.1996.0052"},{"issue":"1-3","key":"8_CR14","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.scico.2004.01.007","volume":"50","author":"U.S. Reddy","year":"2004","unstructured":"Reddy, U.S., 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":"8_CR15","unstructured":"Reynolds, J.C.: The essence of Algol. In: Proceedings of the International Symposium on Algorithmic Languages (1981), Reprinted in [8]"},{"key":"8_CR16","unstructured":"Shinwell, M.R.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, Computer Laboratory, University of Cambridge (December 2004)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. In: Theoretical Computer Science (2005) (To appear)","DOI":"10.1016\/j.tcs.2005.06.003"},{"key":"8_CR18","unstructured":"Sieber, K.: New steps towards full abstraction for local variables. In: Proceedings of the ACM SIGPLAN Workshop on State in Programming Languages (1993)"},{"key":"8_CR19","unstructured":"Stark, I.D.B.: Names and Higher-Order Functions. PhD thesis, Computer Laboratory, University of Cambridge, Available as Technical Report 363 (December 1994)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Sumii, E., Pierce, B.C.: Logical relations for encryption. Journal of Computer Security\u00a011(4) (2003)","DOI":"10.3233\/JCS-2003-11403"},{"issue":"1\/2","key":"8_CR21","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1023\/A:1010022312623","volume":"13","author":"R.D. Tennent","year":"2000","unstructured":"Tennent, R.D., Ghica, D.R.: Abstract models of storage. Higher-Order and Symbolic Computation\u00a013(1\/2), 119\u2013129 (2000)","journal-title":"Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11417170_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T22:10:01Z","timestamp":1740780601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11417170_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255932","9783540320142"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11417170_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}