{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:02Z","timestamp":1780994702012,"version":"3.54.1"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2238744,2340192"],"award-info":[{"award-number":["2238744,2340192"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Live programming environments provide various semantic services, including type checking and evaluation, continuously as the user is editing the program. The live paradigm promises to improve the developer experience, but liveness is an implementation challenge, particularly when working with large programs. This paper specifies and efficiently implements a system that is able to incrementally update type information for a live program in response to fine-grained program edits. This information includes type error marks and information about the expected and actual type of every expression. The system is specified type-theoretically as a small-step dynamics that propagates updates through the marked and annotated program. Most updates flow according to a base bidirectional type system. Additional pointers are maintained to connect bound variables to their binding locations, with type updates traversing these pointers directly. Order maintenance data structures are employed to efficiently maintain these pointers and to prioritize the order of update propagation. We prove this system is equivalent to naive reanalysis in the Agda theorem prover, along with other important metatheoretic properties. We then provide an efficient OCaml implementation, detailing a number of impactful optimizations. We evaluate this implementation's performance with a large stress-test and find that it is able to achieve multiple orders of magnitude speed-up compared to from-scratch reanalysis.<\/jats:p>","DOI":"10.1145\/3763117","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1865-1892","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Incremental Bidirectional Typing via Order Maintenance"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-1809-8382","authenticated-orcid":false,"given":"Thomas J.","family":"Porter","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3418-4835","authenticated-orcid":false,"given":"Marisa","family":"Kirisame","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0286-2808","authenticated-orcid":false,"given":"Ivan","family":"Wei","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2621-3592","authenticated-orcid":false,"given":"Pavel","family":"Panchekha","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4502-7971","authenticated-orcid":false,"given":"Cyrus","family":"Omar","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2018. salsa. https:\/\/github.com\/salsa-rs\/salsa"},{"key":"e_1_2_1_2_1","volume-title":"Self-adjusting computation","author":"Acar Umut A","unstructured":"Umut A Acar. 2005. Self-adjusting computation. Carnegie Mellon University."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503296"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_19"},{"key":"e_1_2_1_5_1","volume-title":"Workshop on Programming for the Planet (PROPL).","author":"Bandukwala Alexander","year":"2024","unstructured":"Alexander Bandukwala, Andrew Blinn, and Cyrus Omar. 2024. Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine. In Workshop on Programming for the Planet (PROPL)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45749-6_17"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_7"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/253262.253266"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567544"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802184"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814277"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 16th edition of the BElgian-NEtherlands software eVOLution symposium, Serge Demeyer, Ali Parsai, Gulsher Laghari, and Brent van Bladel (Eds.) (CEUR Workshop Proceedings","volume":"35","author":"Es Noah Van","year":"2017","unstructured":"Noah Van Es, Maarten Vandercammen, and Coen De Roover. 2017. Incrementalizing Abstract Interpretation. In Proceedings of the 16th edition of the BElgian-NEtherlands software eVOLution symposium, Serge Demeyer, Ali Parsai, Gulsher Laghari, and Brent van Bladel (Eds.) (CEUR Workshop Proceedings, Vol. 2047). CEUR-WS.org, 31\u201335. https:\/\/ceur-ws.org\/Vol-2047\/BENEVOL_2017_paper_9.pdf"},{"key":"e_1_2_1_14_1","unstructured":"Tali Garseil. 2010. How browsers work \u2014 taligarsiel.com. https:\/\/taligarsiel.com\/Projects\/howbrowserswork1.htm####Dirty_bit_system [Accessed 05-11-2024]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Vaidehi Ghime Ankita Khadsare Anushri Jana and Bharti Chimdyalwar. 2022. IR Mapping: Intermediate Representation (IR) based Mapping to facilitate Incremental Static Analysis. In ISEC 2022: 15th Innovations in Software Engineering Conference Saurabh Tiwari Sanjay Chaudhary Chanchal K. Roy Meenakshi D\u2019Souza Richa Sharma and Lov Kumar (Eds.). ACM 23:1\u201323:5. https:\/\/doi.org\/10.1145\/3511430.3511451 10.1145\/3511430.3511451","DOI":"10.1145\/3511430.3511451"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814305"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594324"},{"key":"e_1_2_1_18_1","unstructured":"Amelia Holcomb Michael Dales Patrick Ferris Sadiq Jaffer Thomas Swinfield Alison Eyres Andrew Balmford David Coomes Srinivasan Keshav and Anil Madhavapeddy. 2023. A Case for Planetary Computing. arXiv e-prints arXiv\u20132303."},{"key":"e_1_2_1_19_1","unstructured":"Marisa Kirisame Tiezhi Wang and Pavel Panchekha. 2025. Spineless Traversal for Layout Invalidation. arxiv:2411.10659. arxiv:2411.10659"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_29"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3635800.3637447"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868358.1868363"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2501854"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of CIDR 2013 (proceedings of cidr 2013 ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/differential-dataflow\/","author":"McSherry Frank","year":"2013","unstructured":"Frank McSherry, Derek Murray, Rebecca Isaacs, and Michael Isard. 2013. Differential dataflow. In Proceedings of CIDR 2013 (proceedings of cidr 2013 ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/differential-dataflow\/"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567092"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236774"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54804-8_9"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009900"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SNAPL.2017.11"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428195"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Thomas J. Porter Marisa Kirisame Ivan Wei Pavel Panchekha and Cyrus Omar. 2025. Artifact for Incremental Bidirectional Typing via Order Maintenance. https:\/\/doi.org\/10.5281\/zenodo.16922160 10.5281\/zenodo.16922160","DOI":"10.5281\/zenodo.16922160"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704864"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75305"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.79"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158710"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2025.28"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Helmut Seidl Julian Erhard and Ralf Vogler. 2020. Incremental Abstract Interpretation. In From Lambda Calculus to Cybersecurity Through Program Analysis - Essays Dedicated to Chris Hankin on the Occasion of His Retirement Alessandra Di Pierro Pasquale Malacaria and Rajagopal Nagarajan (Eds.) (Lecture Notes in Computer Science Vol. 12065). Springer 132\u2013148. https:\/\/doi.org\/10.1007\/978-3-030-41103-9_5 10.1007\/978-3-030-41103-9_5","DOI":"10.1007\/978-3-030-41103-9_5"},{"key":"e_1_2_1_39_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop.","author":"Jeremy","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SNAPL.2015.274"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.RTA.2011.345"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970298"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/358746.358755"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02654-1_15"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606713"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629536"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_22"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3479394.3479415"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632910"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763117","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763117","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:47:08Z","timestamp":1760032028000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":50,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763117"],"URL":"https:\/\/doi.org\/10.1145\/3763117","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}