{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T02:43:28Z","timestamp":1790477008470,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,9,12]],"date-time":"2005-09-12T00:00:00Z","timestamp":1126483200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,9,12]]},"DOI":"10.1145\/1086365.1086376","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T12:34:39Z","timestamp":1131366879000},"page":"78-91","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["A step-indexed model of substructural state"],"prefix":"10.1145","author":[{"given":"Amal","family":"Ahmed","sequence":"first","affiliation":[{"name":"Harvard University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Fluet","sequence":"additional","affiliation":[{"name":"Cornell University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[{"name":"Harvard University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2005,9,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"January","author":"Ahmed Amal","year":"2003","unstructured":"Amal Ahmed , Andrew W. Appel , and Roberto Virga . An indexed model of impredicative polymorphism and mutable references. Available at http:\/\/www.cs.princeton.edu\/~appel\/papers\/impred.pdf , January 2003 .]] Amal Ahmed, Andrew W. Appel, and Roberto Virga. An indexed model of impredicative polymorphism and mutable references. Available at http:\/\/www.cs.princeton.edu\/~appel\/papers\/impred.pdf, January 2003.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781146"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021014.79255.33"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645396.651964"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/142137.142162"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040329"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512532"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647979.743374"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029873.1029883"},{"key":"e_1_3_2_1_18_1","first-page":"165","volume-title":"Proc. European Symposium on Programming (ESOP)","author":"Hofmann Martin","year":"2000","unstructured":"Martin Hofmann . A type system for bounded space and functional in-place update . In Proc. European Symposium on Programming (ESOP) , pages 165 -- 179 , March 2000 .]] Martin Hofmann. A type system for bounded space and functional in-place update. In Proc. European Symposium on Programming (ESOP), pages 165--179, March 2000.]]"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503303"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292546"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/647976.743223"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_22"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/331605.331611"},{"key":"e_1_3_2_1_25_1","first-page":"55","volume-title":"Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. Logic in Computer Science (LICS)","author":"John","year":"2002","unstructured":"John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. Logic in Computer Science (LICS) , pages 55 -- 74 , July 2002 .]] John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. Logic in Computer Science (LICS), pages 55--74, July 2002.]]"},{"key":"e_1_3_2_1_26_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/3-540-57787-4_23","volume-title":"Dagstuhl Seminar on Graph Transformations in Computer Science","author":"Smetsers Sjaak","year":"1994","unstructured":"Sjaak Smetsers , Erik Barendsen , Marko C. J. D. van Eekelen , and Rinus J. Plasmeijer . Guaranteeing safe destructive updates through a type system with uniqueness information for graphs . In Dagstuhl Seminar on Graph Transformations in Computer Science , volume 776 of Lecture Notes in Computer Science , pages 358 -- 379 . Springer-Verlag , 1994 .]] Sjaak Smetsers, Erik Barendsen, Marko C. J. D. van Eekelen, and Rinus J. Plasmeijer. Guaranteeing safe destructive updates through a type system with uniqueness information for graphs. In Dagstuhl Seminar on Graph Transformations in Computer Science, volume 776 of Lecture Notes in Computer Science, pages 358--379. Springer-Verlag, 1994.]]"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/645394.651903"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224168"},{"key":"e_1_3_2_1_29_1","volume-title":"April","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . Linear types can change the world! In Programming Concepts and Methods , April 1990 . IFIP TC 2 Working Conference .]] Philip Wadler. Linear types can change the world! In Programming Concepts and Methods, April 1990. IFIP TC 2 Working Conference.]]"},{"key":"e_1_3_2_1_30_1","first-page":"3","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker David","year":"2005","unstructured":"David Walker . Substructural type systems . In Benjamin Pierce, editor, Advanced Topics in Types and Programming Languages , chapter 1, pages 3 -- 43 . MIT Press , Cambridge, MA , 2005 .]] David Walker. Substructural type systems. In Benjamin Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 1, pages 3--43. MIT Press, Cambridge, MA, 2005.]]"},{"key":"e_1_3_2_1_31_1","first-page":"177","volume-title":"Proc. Workshop on Types in Compilation (TIC)","author":"Walker David","year":"2000","unstructured":"David Walker and Greg Morrisett . Alias types for recursive data structures . In Proc. Workshop on Types in Compilation (TIC) , pages 177 -- 206 , September 2000 .]] David Walker and Greg Morrisett. Alias types for recursive data structures. In Proc. Workshop on Types in Compilation (TIC), pages 177--206, September 2000.]]"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507658"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292545"}],"event":{"name":"ICFP05: ACM SIGPLAN International Conference on Functional Programming","location":"Tallinn Estonia","acronym":"ICFP05","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the tenth ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1086365.1086376","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1086365.1086376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:12Z","timestamp":1750248492000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1086365.1086376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,12]]},"references-count":29,"alternative-id":["10.1145\/1086365.1086376","10.1145\/1086365"],"URL":"https:\/\/doi.org\/10.1145\/1086365.1086376","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1090189.1086376","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,9,12]]},"assertion":[{"value":"2005-09-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}