{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T03:20:20Z","timestamp":1778037620273,"version":"3.51.4"},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2010,7,2]],"date-time":"2010-07-02T00:00:00Z","timestamp":1278028800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2010,8]]},"abstract":"<jats:p>We present a realisability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types that include general reference types. The interpretation uses a new approach to modelling references.<\/jats:p><jats:p>The universe of semantic types consists of world-indexed families of logical relations over a universal predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds.<\/jats:p><jats:p>We illustrate how the model can be used to prove simple equivalences between different implementations of imperative abstract data types.<\/jats:p>","DOI":"10.1017\/s0960129510000162","type":"journal-article","created":{"date-parts":[[2010,7,2]],"date-time":"2010-07-02T11:56:11Z","timestamp":1278071771000},"page":"655-703","source":"Crossref","is-referenced-by-count":15,"title":["Realisability semantics of parametric polymorphism, general references and recursive types"],"prefix":"10.1017","volume":"20","author":[{"given":"LARS","family":"BIRKEDAL","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KRISTIAN","family":"ST\u00d8VRING","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JACOB","family":"THAMSBORG","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2010,7,2]]},"reference":[{"key":"S0960129510000162_ref32","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"key":"S0960129510000162_ref31","volume-title":"Handbook of Logic in Computer Science","author":"Smyth","year":"1992"},{"key":"S0960129510000162_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_32"},{"key":"S0960129510000162_ref25","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0960129510000162_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_26"},{"key":"S0960129510000162_ref22","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2845"},{"key":"S0960129510000162_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"S0960129510000162_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035759"},{"key":"S0960129510000162_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_5"},{"key":"S0960129510000162_ref13","doi-asserted-by":"crossref","unstructured":"Birkedal L. , Reus B. , Schwinghammer J. , St\u00f8vring K. , Thamsborg J. and Yang H. (2010a) Step-indexed kripke models over recursive worlds. Submitted for publication. Available at http:\/\/www.itu.dk\/people\/birkedal\/papers\/step-recworld-conf.pdf.","DOI":"10.1145\/1926385.1926401"},{"key":"S0960129510000162_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_8"},{"key":"S0960129510000162_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"S0960129510000162_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983504"},{"key":"S0960129510000162_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.10.002"},{"key":"S0960129510000162_ref2","doi-asserted-by":"crossref","unstructured":"Abadi M. and Plotkin G. D. (1990) A per model of polymorphism and recursive types. In: Proceedings of LICS 355\u2013365.","DOI":"10.1109\/LICS.1990.113761"},{"key":"S0960129510000162_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003054"},{"key":"S0960129510000162_ref26","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"S0960129510000162_ref5","unstructured":"Ahmed A. (2004) Semantics of Types for Mutable State, Ph.D. thesis, Princeton University."},{"key":"S0960129510000162_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"S0960129510000162_ref14","doi-asserted-by":"crossref","unstructured":"Birkedal L. , St\u00f8vring K. and Thamsborg J. (2009) Relational parametricity for references and recursive types. In: Proceedings of TLDI 91\u2013104.","DOI":"10.1145\/1481861.1481873"},{"key":"S0960129510000162_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_2"},{"key":"S0960129510000162_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055063"},{"key":"S0960129510000162_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"S0960129510000162_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211300"},{"key":"S0960129510000162_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480925"},{"key":"S0960129510000162_ref33","unstructured":"Wagner K. R. (1994) Solving Recursive Domain Equations with Enriched Categories, Ph.D. thesis, Carnegie Mellon University."},{"key":"S0960129510000162_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90074-C"},{"key":"S0960129510000162_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"S0960129510000162_ref15","unstructured":"Birkedal L. , St\u00f8vring K. and Thamsborg J. (2010b) A relational realizability model for higher-order stateful ADTs. Submitted for publication. Available at http:\/\/www.itu.dk\/people\/birkedal\/papers\/relrmhoadt.pdf."},{"key":"S0960129510000162_ref34","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"Winskel","year":"1993"},{"key":"S0960129510000162_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129510000162_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"S0960129510000162_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"S0960129510000162_ref3","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705669"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129510000162","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T21:43:15Z","timestamp":1685655795000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129510000162\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,2]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["S0960129510000162"],"URL":"https:\/\/doi.org\/10.1017\/s0960129510000162","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7,2]]}}}