Incremental & Reactive Programming
Compilers that turn plain functional code into computations that redo only what changed.
Most programs throw away their own work: change one cell of a matrix or one row of a table, and the whole computation runs again from scratch. Incremental programming derives from an ordinary functional program a second one that maps a change to the input to the corresponding change to the output, reusing everything that was already computed.
- Reactive programming (early work): rewiring a dataflow graph live without breaking consistency, and collecting the nodes nobody observes any more (LIVE'18, REBLS'19).
- Generic incrementalization, with Timon Böhler: deriving changes from a data type’s own structure, first for polynomial functors (FTfJP'24), then in DeCo, a core calculus mechanized in Lean (OOPSLA'26).
- OOPSLA 2026 DeCo, with a soundness proof fully mechanized in Lean and a published artifact
Timeline
From Debugging Towards Live Tuning of Reactive Applications
Reactive debuggers expose an application’s dataflow graph, but only to look at. Applying edits through the application’s own events and signals, rather than by writing arbitrary variables, propagates every live change consistently along the graph, and is the basis for a sketched tuning framework aimed at domain experts (early work).
Turning Unobservable into Unreachable: Dynamic Reactive Programming without Leaks
A garbage collector approximates “needed” by “reachable”, which is wrong for dataflow graphs whose signals reference each other: a signal is only needed if it is reachable from the host program and can reach back to it. drx, a reactive DSL embedded in Scala, manages references so that unobservable signals become unreachable, and an ordinary collector reclaims exactly the right ones (an in-progress paper).
Links: REBLS 2019 · github
Incrementalizing Polynomial Functors
Incrementalization is usually ad hoc, with a hand-built notion of change for each data structure. Describing a type as a polynomial functor (a shape plus a map from positions to elements) covers every strictly positive inductive type and lets a change structure be derived, covering changes to elements and to shape alike. The constructions are verified in Lean; the paper is the groundwork for DeCo.
Links: FTfJP 2024 · paper · artifact
DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
Domain-specific incrementalization achieves large speedups but generalizes badly; generic techniques treat domain operations as black boxes. DeCo represents type constructors as containers and requires base types to form change structures, so users instantiate it with their own operations and assemble incrementalizations from correct-by-construction combinators. Soundness is mechanized in Lean, with case studies from linear and relational algebra to trees and CRDTs.
Fig. 2 from the paper: instead of rerunning f on each new input, an initialization function i seeds a cache that a difference function d threads forward.
Links: OOPSLA 2026 · paper · artifact · arxiv
Open questions
Directions that come out of the work above, from thesis-sized (BSc/MSc) to PhD-scale:
- Higher-order programs. DeCo is first-order; supporting first-class functions, e.g. via defunctionalization.
- Imperative programs. Modelling statements as functions from input state to output state fits DeCo’s program shape.
- Compilation. Replacing DeCo’s interpreter by a source-to-source transformation and a compiler backend.
- Dynamic shapes. Changes that alter a structure’s shape, not just its elements.
Useful background is functional programming and some Lean or Scala; my Type Systems lecture covers the foundations. If one of these interests you, write me an email.