{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:47Z","timestamp":1750309187589,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,1,9]]},"DOI":"10.1145\/3636501.3636950","type":"proceedings-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T19:39:27Z","timestamp":1704829167000},"page":"75-88","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Unification for Subformula Linking under Quantifiers"],"prefix":"10.1145","author":[{"given":"Ike","family":"Mulder","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Yves Bertot Gilles Kahn and Laurent Th\u00e9ry. 1994. Proof by Pointing. In Theoretical Aspects of Computer Software (LNCS). 141\u2013160. isbn:978-3-540-48383-0 https:\/\/doi.org\/10.1007\/3-540-57887-0_94 10.1007\/3-540-57887-0_94","DOI":"10.1007\/3-540-57887-0_94"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Kaustuv Chaudhuri. 2013. Subformula Linking as an Interaction Method. In ITP (LNCS). 386\u2013401. isbn:978-3-642-39634-2 https:\/\/doi.org\/10.1007\/978-3-642-39634-2_28 10.1007\/978-3-642-39634-2_28","DOI":"10.1007\/978-3-642-39634-2_28"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Kaustuv Chaudhuri. 2021. Subformula Linking for Intuitionistic Logic with Application to Type Theory. In CADE (LNCS). 200\u2013216. isbn:978-3-030-79876-5 https:\/\/doi.org\/10.1007\/978-3-030-79876-5_12 10.1007\/978-3-030-79876-5_12","DOI":"10.1007\/978-3-030-79876-5_12"},{"key":"e_1_3_2_1_6_1","unstructured":"Kaustuv Chaudhuri. 2023. ProfInt Prototype. https:\/\/chaudhuri.info\/research\/profint\/"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Adam Chlipala. 2011. Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic. PLDI. 234\u2013245. https:\/\/doi.org\/10.1145\/1993498.1993526 10.1145\/1993498.1993526","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/362759.362813"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586054"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-B"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","unstructured":"David Delahaye. 2000. A Tactic Language for the System Coq. In LPAR (LNCS). 85\u201395. isbn:978-3-540-44404-6 https:\/\/doi.org\/10.1007\/3-540-44404-1_7 10.1007\/3-540-44404-1_7","DOI":"10.1007\/3-540-44404-1_7"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew J. Parkinson and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP (LNCS). 504\u2013528. isbn:978-3-642-14106-5 https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24 10.1007\/978-3-642-14107-2_24","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Pablo Donato Pierre-Yves Strub and Benjamin Werner. 2022. A Drag-and-Drop Proof Tactic. In CPP. 197\u2013209. isbn:978-1-4503-9182-5 https:\/\/doi.org\/10.1145\/3497775.3503692 10.1145\/3497775.3503692","DOI":"10.1145\/3497775.3503692"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. LICS. 442\u2013451. isbn:978-1-4503-5583-4 https:\/\/doi.org\/10.1145\/3209108.3209174 10.1145\/3209108.3209174","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle Semantics for Concurrent Separation Logic. In ESOP (LNCS). 353\u2013367. isbn:978-3-540-78739-6 https:\/\/doi.org\/10.1007\/978-3-540-78739-6_27 10.1007\/978-3-540-78739-6_27","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-Order Ghost State. ICFP. 256\u2013269. isbn:978-1-4503-4219-3 https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_3_2_1_23_1","volume-title":"Coq Workshop. https:\/\/github.com\/uds-psl\/coq-library-fol","author":"Kirst Dominik","year":"2022","unstructured":"Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas M\u00fcck, Benjamin Peters, Gert Smolka, and Wehr, Dominik. 2022. A Coq Library for Mechanised First-Order Logic. In Coq Workshop. https:\/\/github.com\/uds-psl\/coq-library-fol"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ale\u0161 Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP (LNCS). 696\u2013723. isbn:978-3-662-54434-1 https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. POPL. 205\u2013217. isbn:978-1-4503-4660-3 https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591275"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Ike Mulder and Robbert Krebbers. 2023. Artifact of \u2018Unification for Subformula Linking under Quantifiers\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.10364816 10.5281\/zenodo.10364816","DOI":"10.5281\/zenodo.10364816"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586043"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Peter O\u2019Hearn John Reynolds and Hongseok Yang. 2001. Local Reasoning about Programs That Alter Data Structures. In CSL (LNCS). 1\u201319. isbn:978-3-540-44802-0 https:\/\/doi.org\/10.1007\/3-540-44802-0_1 10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications (Applied Logic Series","author":"Pym David J.","key":"e_1_3_2_1_33_1","unstructured":"David J. Pym. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications (Applied Logic Series, Vol. 26). Kluwer. isbn:978-1-4020-0745-3"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. PLDI. 158\u2013174. isbn:978-1-4503-8391-2 https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In TPHOLs (LNCS). 278\u2013293. isbn:978-3-540-71067-7 https:\/\/doi.org\/10.1007\/978-3-540-71067-7_23 10.1007\/978-3-540-71067-7_23","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Matthieu Sozeau and Nicolas Tabareau. 2014. Universe Polymorphism in Coq. In ITP (LNCS). 499\u2013514. isbn:978-3-319-08970-6 https:\/\/doi.org\/10.1007\/978-3-319-08970-6_32 10.1007\/978-3-319-08970-6_32","DOI":"10.1007\/978-3-319-08970-6_32"},{"key":"e_1_3_2_1_38_1","unstructured":"The Coq-std++ Team. 2023. An Extended \"Standard Library\" for Coq.. https:\/\/gitlab.mpi-sws.org\/iris\/stdpp"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Beta Ziliani and Matthieu Sozeau. 2015. A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading. ICFP. 179\u2013191. isbn:978-1-4503-3669-7 https:\/\/doi.org\/10.1145\/2784731.2784751 10.1145\/2784731.2784751","DOI":"10.1145\/2784731.2784751"}],"event":{"name":"CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"London UK","acronym":"CPP '24"},"container-title":["Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636950","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636501.3636950","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:11Z","timestamp":1750287251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636950"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,9]]},"references-count":39,"alternative-id":["10.1145\/3636501.3636950","10.1145\/3636501"],"URL":"https:\/\/doi.org\/10.1145\/3636501.3636950","relation":{},"subject":[],"published":{"date-parts":[[2024,1,9]]},"assertion":[{"value":"2024-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}