{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:22:25Z","timestamp":1765617745031,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100003062","name":"ERC","doi-asserted-by":"publisher","award":["101171349"],"award-info":[{"award-number":["101171349"]}],"id":[{"id":"10.13039\/501100003062","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,10]]},"DOI":"10.1145\/3756907.3756909","type":"proceedings-article","created":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:11Z","timestamp":1765617551000},"page":"1-2","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanized Type Soundness for Substructural Types using Iris"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,12,13]]},"reference":[{"key":"e_1_3_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1037736"},{"key":"e_1_3_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325727"},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Andrew\u00a0W. Appel and David\u00a0A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. TOPLAS 23 5 (2001) 657\u2013683. 10.1145\/504709.504712","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Stephen Brookes. 2007. A semantics for concurrent separation logic. TCS 375 1-3 (2007) 227\u2013270. 10.1016\/J.TCS.2006.12.034","DOI":"10.1016\/J.TCS.2006.12.034"},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Simon\u00a0J. Gay and Vasco\u00a0Thudichum Vasconcelos. 2010. Linear type theory for asynchronous session types. JFP 20 1 (2010) 19\u201350. 10.1017\/S0956796809990268","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_3_3_1_8_2","doi-asserted-by":"publisher","unstructured":"Jonas\u00a0Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2020. Actris: session-type based reasoning in separation logic. PACMPL 4 POPL (2020) 6:1\u20136:30. 10.1145\/3371074","DOI":"10.1145\/3371074"},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0053567"},{"key":"e_1_3_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Jules Jacobs Jonas\u00a0Kastberg Hinrichsen and Robbert Krebbers. 2024. Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. PACMPL 8 POPL (2024) 1385\u20131417. 10.1145\/3632889","DOI":"10.1145\/3632889"},{"key":"e_1_3_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP 28 (2018) e20. 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A general extensible modal framework for interactive proofs in separation logic. PACMPL 2 ICFP (2018) 77:1\u201377:30. 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Robin Milner. 1978. A Theory of Type Polymorphism in Programming. JCSS 17 3 (1978) 348\u2013375. 10.1016\/0022-0000(78)90014-4","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Peter\u00a0W. O\u2019Hearn. 2007. Resources concurrency and local reasoning. TCS 375 1-3 (2007) 271\u2013307. 10.1016\/J.TCS.2006.12.035","DOI":"10.1016\/J.TCS.2006.12.035"},{"key":"e_1_3_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. JACM 71 6 (2024) 40:1\u201340:75. 10.1145\/3676954","DOI":"10.1145\/3676954"},{"key":"e_1_3_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Andrew\u00a0K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. I&C 115 1 (1994) 38\u201394. 10.1006\/INCO.1994.1093","DOI":"10.1006\/INCO.1994.1093"}],"event":{"name":"PPDP '25: Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming","location":"Rende Italy","acronym":"PPDP '25"},"container-title":["Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3756907.3756909","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:57Z","timestamp":1765617597000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3756907.3756909"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,10]]},"references-count":21,"alternative-id":["10.1145\/3756907.3756909","10.1145\/3756907"],"URL":"https:\/\/doi.org\/10.1145\/3756907.3756909","relation":{},"subject":[],"published":{"date-parts":[[2025,9,10]]},"assertion":[{"value":"2025-12-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}