{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:23Z","timestamp":1750309523125,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"This work was funded by the Natural Sciences and Engineering Research Council of Canada and the Fonds de recherche du Quebec --- Nature et technologies.","award":[""],"award-info":[{"award-number":[""]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705888","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"257-271","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Split Decisions: Explicit Contexts for Substructural Languages"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6153-2955","authenticated-orcid":false,"given":"Daniel","family":"Zackon","sequence":"first","affiliation":[{"name":"McGill University, Montreal, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8179-2307","authenticated-orcid":false,"given":"Chuta","family":"Sano","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0942-4777","authenticated-orcid":false,"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[{"name":"University of Milan, Milan, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2549-4276","authenticated-orcid":false,"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, Canada"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2017.1"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"volume-title":"Dual intuitionistic linear logic","author":"Barber Andrew","key":"e_1_3_2_2_3_1","unstructured":"Andrew Barber. 1996. Dual intuitionistic linear logic. University of Edinburgh. https:\/\/www.lfcs.inf.ed.ac.uk\/reports\/96\/ECS-LFCS-96-347"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_2_7_1","volume-title":"Proc. TLLA \u201921","author":"Callies \u00c9tienne","year":"2021","unstructured":"\u00c9tienne Callies and Olivier Laurent. 2021. Click and coLLecT: An interactive linear logic prover. In Proc. TLLA \u201921. https:\/\/hal-lirmm.ccsd.cnrs.fr\/lirmm-03271501"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-62697-5_9"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_17"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.2001.2951"},{"volume-title":"Separation Logic Foundations (Software Foundations","author":"Chargu\u00e9raud Arthur","key":"e_1_3_2_2_11_1","unstructured":"Arthur Chargu\u00e9raud. 2024. Separation Logic Foundations (Software Foundations, Vol. 6). Electronic textbook. Version 2.2."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.02.023"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414109"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.116"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863565"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.06.002"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-010-9194-X"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9327-3"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000323"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_16"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_20"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000231"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.404.2"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2024.15"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_3_2_2_33_1","unstructured":"Olivier Laurent. 2017. Yalla. https:\/\/github.com\/olaure01\/yalla\/"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001131"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000366"},{"key":"e_1_3_2_2_43_1","unstructured":"Klaas Pruiksma William Chargin Frank Pfenning and Jason Reed. 2018. Adjoint logic. April https:\/\/www.cs.cmu.edu\/~fp\/papers\/adjoint18b.pdf (unpublished manuscript)."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2003.11.020"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2006.11.030"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373818"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622810"},{"key":"e_1_3_2_2_48_1","unstructured":"Anders Schack-Nielsen. 2011. Implementing Substructural Logical Frameworks. Ph.D. Dissertation. Copenhagen Denmark. isbn:978-87-7949236-3"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_28"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_1"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005238"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354184"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"volume-title":"Advanced Topics in Types and Programming Languages, Benjamin C","author":"Walker David","key":"e_1_3_2_2_55_1","unstructured":"David Walker. 2005. Substructural type systems. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, 3\u201343."},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.353.10"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_14"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2018.10.014"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14271731"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78089-0_9"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"location":"Denver CO USA","acronym":"CPP '25"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705888","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705888","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705888"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":60,"alternative-id":["10.1145\/3703595.3705888","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705888","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}