Incremental computing offers the potential for significant performance gains by efficiently updating computations in response to changing data. However, traditional approaches are either problem-specific or use an inefficient all-or-nothing strategy of rerunning affected computations entirely. This paper presents differential semantics, a novel approach that directly embeds the propagation of changes into the semantics of a general-purpose programming language. Given a precise description of input changes, differential semantics rules define how these changes are tracked and propagated through core language constructs like assignments, conditionals, and loops to produce corresponding output changes. We formalize differential semantics and verify key properties, including correctness, using the Rocq proof assistant. We also develop and formally prove a set of optimizations, particularly for loop handling, that enable asymptotic performance improvements. An implementation of the semantics as a differential interpreter achieves order-of-magnitude speedups over recomputation on the Bellman-Ford shortest path algorithm.
@InProceedings{kumar_et_al:LIPIcs.ECOOP.2025.20, author = {Kumar, Prashant and Pacak, Andr\'{e} and Erdweg, Sebastian}, title = {{Incremental Computing by Differential Execution}}, booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)}, pages = {20:1--20:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-373-7}, ISSN = {1868-8969}, year = {2025}, volume = {333}, editor = {Aldrich, Jonathan and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.20}, URN = {urn:nbn:de:0030-drops-233137}, doi = {10.4230/LIPIcs.ECOOP.2025.20}, annote = {Keywords: Incremental computing, differential semantics, programming language design, formal verification, big-step semantics} }
Feedback for Dagstuhl Publishing