{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:07Z","timestamp":1753889707079,"version":"3.41.2"},"reference-count":26,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T00:00:00Z","timestamp":1344556800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We investigate the problem of type isomorphisms in the presence of higher-order references. We first introduce a finitary programming language with sum types and higher-order references, for which we build a fully abstract games model following the work of Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in our language. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding new non-trivial type isomorphisms in a variant of our language with natural numbers.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:8)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":3,"title":["Isomorphisms of types in the presence of higher-order references (extended version)"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Pierre","family":"Clairambault","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,8,10]]},"reference":[{"unstructured":"S. Abramsky, K. Honda, and G. McCusker. A fully abstract game semantics for general references. In13th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1998.","key":"10.2168\/LMCS-8(3:8)2012_ahm"},{"doi-asserted-by":"crossref","unstructured":"S. Abramsky and G. McCusker. Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions, 1997. S. Abramsky and G. McCusker. Call-by-value games. In Mogens Nielsen and Wolfgang Thomas, editors,6th Annual Conference of the European Association for Computer Science Logic, volume 1414 ofLecture Notes in Computer Science. Springer, 1998.","key":"10.2168\/LMCS-8(3:8)2012_abramsky-mccusker:active-algol","DOI":"10.1007\/978-1-4757-3851-3_10"},{"doi-asserted-by":"crossref","unstructured":"F. Atanassow and J. Jeuring. Inferring type isomorphisms generically. In Dexter Kozen and Carron Shankland, editors,MPC, volume 3125 ofLecture Notes in Computer Science, pages 32-53. Springer, 2004.","key":"10.2168\/LMCS-8(3:8)2012_DBLP:conf\/mpc\/AtanassowJ04","DOI":"10.1007\/978-3-540-27764-4_4"},{"doi-asserted-by":"crossref","unstructured":"G. Barthe and O. Pons. Type isomorphisms and proof reuse in dependent type theory. In Furio Honsell and Marino Miculan, editors,FoSSaCS, volume 2030 ofLecture Notes in Computer Science, pages 57-71. Springer, 2001.","key":"10.2168\/LMCS-8(3:8)2012_DBLP:conf\/fossacs\/BartheP01","DOI":"10.1007\/3-540-45315-6_4"},{"key":"10.2168\/LMCS-8(3:8)2012_berry-curien","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/S0304-3975(82)80002-9","volume":"20","author":"G. Berry and P.-L. Curien","year":"1982","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/mscs\/BruceCL92","first-page":"231","volume":"2","author":"K.B. Bruce, R. Di Cosmo, and G. Longo","year":"1992","journal-title":"Mathematical Structures in Computer Science 1992"},{"doi-asserted-by":"crossref","unstructured":"K.B. Bruce and G. Longo. Provable isomorphisms and domain equations in models of typed languages (preliminary version). InSTOC, pages 263-272. ACM, 1985.","key":"10.2168\/LMCS-8(3:8)2012_DBLP:conf\/stoc\/BruceL85","DOI":"10.1145\/22145.22175"},{"issue":"3","key":"10.2168\/LMCS-8(3:8)2012_dezani1976characterization","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(76)90085-2","volume":"2","author":"M. Dezani-Ciancaglini","year":"1976","journal-title":"Theoretical Computer Science"},{"unstructured":"R. Di Cosmo. Invertibility of terms and valid isomorphisms, a proof theoretic study on second order lambda-calculus with surjective pairing and terminal object. Technical report, Technical Report TR 10-91, LIENS Ecole Normale Sup\u00e9rieure, Paris, 1991.","key":"10.2168\/LMCS-8(3:8)2012_diinvertibility"},{"issue":"5","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/mscs\/Cosmo05","doi-asserted-by":"crossref","first-page":"825","DOI":"10.1017\/S0960129505004871","volume":"15","author":"R. Di Cosmo","year":"2005","journal-title":"Mathematical Structures in Computer Science 2005"},{"issue":"1-2","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/apal\/FioreCB06","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.apal.2005.09.001","volume":"141","author":"M. Fiore, R. Di Cosmo, and V. Balat","year":"2006","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1-2","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/tcs\/HondaY99","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1016\/S0304-3975(99)00039-0","volume":"221","author":"K. Honda and N. Yoshida","year":"1999","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"10.2168\/LMCS-8(3:8)2012_hyland-ong","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"J.M.E. Hyland and C.H.L. Ong","year":"2000","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland and A. Schalk. Games on graphs and sequentially realizable functionals. InLogic in Computer Science 02, pages 257-264, Kopenhavn, July 2002. IEEE Computer Society Press.","key":"10.2168\/LMCS-8(3:8)2012_hyland-schalk","DOI":"10.1109\/LICS.2002.1029834"},{"issue":"447-468","key":"10.2168\/LMCS-8(3:8)2012_joyal-street-verity","first-page":"184","volume":"119","author":"A. Joyal, R. Street, and D. Verity","year":"1996","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"doi-asserted-by":"crossref","unstructured":"J. Laird. Full abstraction for functional languages with control. In12th IEEE Symposium on Logic in Computer Science, pages 58-67, 1997.","key":"10.2168\/LMCS-8(3:8)2012_laird97","DOI":"10.1109\/LICS.1997.614931"},{"doi-asserted-by":"crossref","unstructured":"J. Laird. A game semantics of the asynchronouspi-calculus. InCONCUR, pages 51-65, 2005.","key":"10.2168\/LMCS-8(3:8)2012_DBLP:conf\/concur\/Laird05","DOI":"10.1007\/11539452_8"},{"issue":"1-3","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/apal\/Laurent04","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.apal.2004.04.006","volume":"130","author":"O. Laurent","year":"2004","journal-title":"Annals of Pure and Applied Logic"},{"issue":"5","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/mscs\/Laurent05","doi-asserted-by":"crossref","first-page":"969","DOI":"10.1017\/S0960129505004895","volume":"15","author":"O. Laurent","year":"2005","journal-title":"Mathematical Structures in Computer Science 2005"},{"doi-asserted-by":"crossref","unstructured":"G. McCusker. Games and full abstraction for a functional metalanguage with recursive types. PhD thesis, Imperial College, University of London, 1996. Published in Springer-Verlag's Distinguished Dissertations in Computer Science series, 1998.","key":"10.2168\/LMCS-8(3:8)2012_McCusker1996","DOI":"10.1007\/978-1-4471-0615-9_3"},{"key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/entcs\/MelliesT09","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1016\/j.entcs.2009.07.099","volume":"249","author":"P.-A. Melli\u00e8s and N. Tabareau","year":"2009","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10.2168\/LMCS-8(3:8)2012_moggi","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","journal-title":"Information and Computation"},{"author":"A. Murawski and N. Tzevelekos","journal-title":"In Luca de Alfaro, editor, FOSSACS Notes in Computer Science}, pages 32-47. Springer, 2009","key":"10.2168\/LMCS-8(3:8)2012_DBLP:conf\/fossacs\/MurawskiT09"},{"doi-asserted-by":"crossref","unstructured":"A. Murawski and N. Tzevelekos. Game semantics for good general references. InLICS, pages 75-84. IEEE Computer Society, 2011.","key":"10.2168\/LMCS-8(3:8)2012_DBLP:conf\/lics\/MurawskiT11","DOI":"10.1109\/LICS.2011.31"},{"issue":"1","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/jfp\/Rittri91","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1017\/S095679680000006X","volume":"1","author":"M. Rittri","year":"1991","journal-title":"J. Funct. Program."},{"issue":"6","key":"10.2168\/LMCS-8(3:8)2012_DBLP:journals\/ita\/Rittri93","first-page":"523","volume":"27","author":"M. Rittri","year":"1993","journal-title":"ITA"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1040\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1040\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:26:26Z","timestamp":1746059186000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,10]]},"references-count":26,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:8)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1207.3223","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1207.3223","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,8,10]]},"article-number":"1040"}}