{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T11:38:42Z","timestamp":1753357122253},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"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-04027-6_33","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T13:27:52Z","timestamp":1252934872000},"page":"455-469","source":"Crossref","is-referenced-by-count":14,"title":["A Complete Characterization of Observational Equivalence in Polymorphic \u03bb-Calculus with General References"],"prefix":"10.1007","author":[{"given":"Eijiro","family":"Sumii","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: Thirteenth Annual IEEE Symposium on Logic in Computer Science, pp. 334\u2013344 (1998)","DOI":"10.1109\/LICS.1998.705669"},{"key":"33_CR2","unstructured":"Ahmed, A., Appel, A.W., Virga, R.: An indexed model of impredicative polymorphism and mutable references (2003), http:\/\/www.cs.princeton.edu\/~amal\/papers\/impred.pdf"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 340\u2013353 (2009)","DOI":"10.1145\/1594834.1480925"},{"issue":"5","key":"33_CR4","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems\u00a023(5), 657\u2013683 (2001)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/978-3-642-00596-1_32","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Birkedal","year":"2009","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Realizability semantics of parametric polymorphism, references, and recursive types. In: Foundations of Software Science and Computation Structures. LNCS, vol.\u00a05504, pp. 456\u2013470. Springer, Heidelberg (2009)"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Relational parametricity for references and recursive types. In: Types in Language Design and Implementation, pp. 91\u2013104 (2009)","DOI":"10.1145\/1481861.1481873"},{"key":"33_CR7","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":"33_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: 14th Annual IEEE Symposium on Logic in Computer Science, pp. 214\u2013224 (1999)","DOI":"10.1109\/LICS.1999.782617"},{"key":"33_CR9","unstructured":"Gordon, A.D.: Functional Programming and Input\/Output. PhD thesis, University of Cambridge (1993)"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 141\u2013152 (2006)","DOI":"10.1145\/1111037.1111050"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/978-3-540-73420-8_58","volume-title":"Automata, Languages and Programming","author":"J. Laird","year":"2007","unstructured":"Laird, J.: A fully abstract trace semantics for general references. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol.\u00a04596, pp. 667\u2013679. Springer, Heidelberg (2007)"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Lassen, S.B., Levy, P.B.: Typed normal form bisimulation for parametric polymorphism. In: 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 341\u2013352 (2008)","DOI":"10.1109\/LICS.2008.26"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables: Preliminary report. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 191\u2013203 (1988)","DOI":"10.1145\/73560.73577"},{"key":"33_CR14","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/B978-0-12-450010-5.50023-2","volume-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","author":"J.C. Mitchell","year":"1991","unstructured":"Mitchell, J.C.: On the equivalence of data representations. In: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 305\u2013330. Academic Press, London (1991)"},{"key":"33_CR15","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"issue":"3","key":"33_CR16","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1145\/337244.337261","volume":"47","author":"B.C. Pierce","year":"2000","unstructured":"Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM\u00a047(3), 531\u2013586 (2000); Extended abstract appeared in: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 531\u2013584 (1997)","journal-title":"Journal of the ACM"},{"key":"33_CR17","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics","author":"A.M. Pitts","year":"1998","unstructured":"Pitts, A.M., Stark, I.: Operational reasoning for functions with local state. In: Higher Order Operational Techniques in Semantics, pp. 227\u2013273. Cambridge University Press, Cambridge (1998)"},{"key":"33_CR18","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing 1983, Proceedings of the IFIP 9th World Computer Congres, pp. 513\u2013523 (1983)"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Twenty-Second Annual IEEE Symposium on Logic in Computer Science, pp. 293\u2013302 (2007)","DOI":"10.1109\/LICS.2007.17"},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/BFb0084781","volume-title":"CONCUR \u201992","author":"D. Sangiorgi","year":"1992","unstructured":"Sangiorgi, D., Milner, R.: The problem of \u201cweak bisimulation up to\u201d. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 32\u201346. Springer, Heidelberg (1992)"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"St\u00f8vring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161\u2013172 (2007)","DOI":"10.1145\/1190216.1190244"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-642-00590-9_18","volume-title":"18th European Symposium on Programming","author":"E. Sumii","year":"2009","unstructured":"Sumii, E.: A theory of non-monotone memory (or: Contexts for free). In: 18th European Symposium on Programming. LNCS, vol.\u00a05502, pp. 237\u2013251. Springer, Heidelberg (2009)"},{"issue":"1\u20133","key":"33_CR23","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.tcs.2006.12.032","volume":"375","author":"E. Sumii","year":"2007","unstructured":"Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. Theoretical Computer Science\u00a0375(1\u20133), 169\u2013192 (2007); Extended abstract appeared in: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.\u00a0161\u2013172 (2004)","journal-title":"Theoretical Computer Science"},{"issue":"5-26","key":"33_CR24","first-page":"1","volume":"54","author":"E. Sumii","year":"2007","unstructured":"Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. Journal of the ACM\u00a054(5-26), 1\u201343 (2007); Extended abstract appeared in: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.\u00a063\u201374 (2005)","journal-title":"Journal of the ACM"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Tzevelekos, N.: Full abstraction for nominal general references. In: Twenty-Second Annual IEEE Symposium on Logic in Computer Science, pp. 399\u2013410 (2007)","DOI":"10.1109\/LICS.2007.21"},{"key":"33_CR26","first-page":"347","volume-title":"Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming Languages and Computer Architecture","author":"P. Wadler","year":"1989","unstructured":"Wadler, P.: Theorems for free! In: Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming Languages and Computer Architecture, pp. 347\u2013359. ACM Press, New York (1989)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T11:19:26Z","timestamp":1558523966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}