{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:00:24Z","timestamp":1767927624608,"version":"3.49.0"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100014013","name":"UKRI","doi-asserted-by":"crossref","award":["Future Leaders Fellowship MR\/T043830\/1 (EHOP)"],"award-info":[{"award-number":["Future Leaders Fellowship MR\/T043830\/1 (EHOP)"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.<\/jats:p>","DOI":"10.1145\/3656398","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"518-542","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["The Functional Essence of Imperative Binary Search Trees"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3538-9688","authenticated-orcid":false,"given":"Anton","family":"Lorenzen","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1027-5430","authenticated-orcid":false,"given":"Daan","family":"Leijen","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0295-7944","authenticated-orcid":false,"given":"Wouter","family":"Swierstra","sequence":"additional","affiliation":[{"name":"Utrecht University, Utrecht, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1360-4714","authenticated-orcid":false,"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000885"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/322092.322094"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.8"},{"key":"e_1_3_1_6_1","unstructured":"Appel. 2018. Software Foundations Volume 3: Verified Functional Algorithms. Electronic textbook."},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE52586.2021.00017"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006399"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Blelloch Ferizovic and Sun. 2016. Just Join for Parallel Ordered Sets. In Proceedings of the 28th ACM Symposium on Parallelism in Algorithms and Architectures 253\u2013264. https:\/\/doi.org\/10.1145\/2935764.2935768 10.1145\/2935764.2935768","DOI":"10.1145\/2935764.2935768"},{"key":"e_1_3_1_11_1","volume-title":"Journe\u00e9es Francophones Des Langages Applicatifs (JFLA)","author":"Bour Cl\u00e9ment","year":"2021","unstructured":"Bour, Cl\u00e9ment, and Scherer. Apr. 2021. Tail Modulo Cons. Journe\u00e9es Francophones Des Langages Applicatifs (JFLA), April. Saint M\u00e9dard d'Excideuil, France. https:\/\/hal.inria.fr\/hal-03146495\/document. hal-03146495."},{"key":"e_1_3_1_12_1","unstructured":"Cao Wang Hobor and Appel. 2019. Proof Pearl: Magic Wand as Frame. arXiv Preprint arXiv:1909.08789."},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud. 2016. Higher-Order Representation Predicates in Separation Logic. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs 3\u201314. https:\/\/doi.org\/10.1145\/2854065.2854068 10.1145\/2854065.2854068","DOI":"10.1145\/2854065.2854068"},{"key":"e_1_3_1_14_1","unstructured":"Clark and T\u00e4rnlund. 1977. A First Order Theory of Data and Programs. In IFIP Congress 939\u2013944."},{"key":"e_1_3_1_15_1","volume-title":"Introduction to Algorithms","author":"Cormen Leiserson","year":"2022","unstructured":"Cormen, Leiserson, Rivest, and Stein. 2022. Introduction to Algorithms. MIT press."},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Danvy and Nielsen. 2001. Defunctionalization at Work. In Proceedings of the 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming 162\u2013174. https:\/\/doi.org\/10.1145\/773184.773202 10.1145\/773184.773202","DOI":"10.1145\/773184.773202"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_5"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_7"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Erbsen Gruetter Choi Wood and Chlipala. 2021. Integration Verification across Software and Hardware for a Simple Embedded System. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation 604\u2013619. https:\/\/doi.org\/10.1145\/3410295 10.1145\/3410295","DOI":"10.1145\/3410295"},{"key":"e_1_3_1_20_1","volume-title":"Unwinding Stylized Recursion into Iterations. 19","author":"Friedman Wise.","year":"1975","unstructured":"Friedman, and Wise. Dec. 1975. Unwinding Stylized Recursion into Iterations. 19. Bloomingdale, Indiana. https:\/\/legacy.cs.indiana.edu\/ftp\/techreports\/TR19.pdf."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Frumin Gondelman and Krebbers. 2019. Semi-Automated Reasoning About Non-Determinism in C Expressions. In ESOP 60\u201387. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_3 10.1007\/978-3-030-17184-1_3","DOI":"10.1007\/978-3-030-17184-1_3"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319309"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1978.3"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45442-X_10"},{"key":"e_1_3_1_25_1","volume-title":"In-Place Update with Linear Types or How to Compile Functional Programms into Malloc-Free C. Preprint","year":"2000","unstructured":"Hofmann. 2000. In-Place Update with Linear Types or How to Compile Functional Programms into Malloc-Free C. Preprint. Citeseer."},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Huet. 1997. The Zipper. Journal of Functional Programming 7 (5): 549\u2013554. https:\/\/doi.org\/10.1017\/S0956796897002864 10.1017\/S0956796897002864","DOI":"10.1017\/S0956796897002864"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0253-9_4"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90059-1"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_18"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types. In MSFP'14 5th Workshop on Mathematically Structured Functional Programming. https:\/\/doi.org\/10.4204\/EPTCS.153.8 10.4204\/EPTCS.153.8","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_3_1_32_1","unstructured":"Leijen. 2021. The Koka Language. https:\/\/koka-lang.github.io."},{"key":"e_1_3_1_33_1","volume-title":"Tail Recursion Modulo Context \u2013 An Equational Approach. MSR-TR-2022-18","year":"2022","unstructured":"Leijen, and Lorenzen. Jul. 2022. Tail Recursion Modulo Context \u2013 An Equational Approach. MSR-TR-2022-18. Microsoft Research."},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Leijen and Lorenzen. Jan. 2023. Tail Recursion Modulo Context: An Equational Approach. Proc. ACM Program. Lang. 7 (POPL). https:\/\/doi.org\/10.1145\/3571233 10.1145\/3571233 See also [Leijen and Lorenzen 2022].","DOI":"10.1145\/3571233"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_13"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547634"},{"key":"e_1_3_1_38_1","volume-title":"FP2 : Fully in-Place Functional Programming","author":"Lorenzen Leijen","year":"2023","unstructured":"Lorenzen, Leijen, and Swierstra. May 2023. FP2 : Fully in-Place Functional Programming. MSR-TR-2023-19. Microsoft Research."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607840"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Lorenzen Leijen Swierstra and Lindley. Mar. 2024. The Functional Essence of Imperative Binary Search Trees (Artifact). Zenodo. https:\/\/doi.org\/10.5281\/zenodo.10790231 10.5281\/zenodo.10790231 Artifact for PLDI'24.","DOI":"10.5281\/zenodo.10790231"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.02.001"},{"key":"e_1_3_1_42_1","unstructured":"McBride. 2001. The Derivative of a Regular Type Is Its Type of One-Hole Contexts. http:\/\/strictlypositive.org\/diff.pdf. (Extended Abstract)."},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"McBride. 2008. Clowns to the Left of Me Jokers to the Right (pearl) Dissecting Data Structures. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 287\u2013295. https:\/\/doi.org\/10.1145\/1328897.1328474 10.1145\/1328897.1328474","DOI":"10.1145\/1328897.1328474"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268953"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591275"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","unstructured":"Mulder Krebbers and Geuvers. 2022. Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation 809\u2013824. https:\/\/doi.org\/10.1145\/3519939.3523432 10.1145\/3519939.3523432","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_1_47_1","unstructured":"Munch-Maccagnoni and Douence. 2019. Efficient Deconstruction with Typed Pointer Reversal. In ML 2019-Workshop 1\u20138"},{"key":"e_1_3_1_48_1","unstructured":"Nipkow Blanchette Eberl G\u00f3mez-Londo\u00f1o Lammich Sternagel Wimmer and Zhan. 2021. Functional Algorithms Verified."},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_2"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003494"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/580840"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594325"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Pit-Claudel Philipoom Jamner Erbsen and Chlipala. 2022. Relational Compilation for Performance-Critical Applications: Extensible Proof-Producing Translation of Functional Models into Low-Level Code. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation 918\u2013933. https:\/\/doi.org\/10.1145\/3519939.3523706 10.1145\/3519939.3523706","DOI":"10.1145\/3519939.3523706"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500598"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/78973.78977"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_60_1","volume-title":"Inst. f\u00f6r Informationsbehandling","year":"1973","unstructured":"Risch. Nov. 1973. REMREC - A Program for Automatic Recursion Removal. Inst. f\u00f6r Informationsbehandling, Uppsala Universitet. https:\/\/user.it.uu.se\/~torer\/publ\/remrec.pdf."},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-25803-9_8"},{"key":"e_1_3_1_62_1","unstructured":"Schmidt. 1997. The GNU C Library tsearch. https:\/\/github.com\/lattera\/glibc\/blob\/master\/misc\/tsearch.c."},{"key":"e_1_3_1_63_1","first-page":"41","volume-title":"Information Processing Letters 45 (1)","year":"1993","unstructured":"Schoenmakers. 1993. A Systematic Analysis of Splaying. Information Processing Letters 45 (1). Elsevier: 41\u201350. https:\/\/doi. org\/10.1016\/0020-0190(93)90249-9."},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/363534.363554"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3794-8_16"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3835"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984027"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00995807"},{"key":"e_1_3_1_69_1","volume-title":"TR-006-85","year":"1985","unstructured":"Tarjan. May 1985. Efficient Top-Down Updating of Red-Black Trees. TR-006-85. Princeton University. https:\/\/www.cs.princeton.edu\/research\/techreps\/TR-006-85."},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3476830"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. Oct. 2017. The Coq Proof Assistant Version 8.7.0. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.1028037 10.5281\/zenodo.1028037","DOI":"10.5281\/zenodo.1028037"},{"key":"e_1_3_1_72_1","unstructured":"The Iris Team. 2022. The Iris 4.0 Reference. https:\/\/plv.mpi-sws.org\/iris."},{"key":"e_1_3_1_73_1","unstructured":"Tuerk. 2010. Local Reasoning about While-Loops. VSTTE 2010: 29."},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412932.3412935"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","unstructured":"Wadler. 1984. Listlessness Is Better than Laziness: Lazy Evaluation and Garbage Collection at Compile-Time. In Proceedings of the 1984 ACM Symposium on LISP and Functional Programming 45\u201352. https:\/\/doi.org\/10.1145\/800055.802020 10.1145\/800055.802020","DOI":"10.1145\/800055.802020"},{"key":"e_1_3_1_76_1","volume-title":"Data Structures and Algorithm Analysis in C++ (Fourth Edition)","year":"2013","unstructured":"Weiss. 2013. Data Structures and Algorithm Analysis in C++ (Fourth Edition). Addison-Wesley."},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_2"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:38Z","timestamp":1751661578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":76,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656398"],"URL":"https:\/\/doi.org\/10.1145\/3656398","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}