Title:      Stateful Differential Operators for Incremental Computing

Speaker:   Runqing Xu ,Karlsruhe Institute of Technology (KIT)   

Time:    27 February 2026 , 10:00 – 11:00

Venue:   Second Meeting Room, 4th Floor, Building 5,ISCAS

Abstract:  

Differential operators map input changes to output changes and form the building blocks of efficient incremental computations. For example, differential operators for relational algebra are used to perform live view maintenance in database systems. However, few differential operators are known and it is unclear how to develop and verify new efficient operators. In particular, we found that differential operators often need to use internal state to selectively cache relevant information, which is not supported by prior work.

To this end, we designed a specification for stateful differential operators that allows custom state, yet places sufficient constraints to ensure correctness. We model our specification in Rocq and show that the specification not only guides the design of novel differential operators, but also can capture some of the most sophisticated existing differential operators, for instances, database join and Datalog aggregation. We show how to describe complex incremental computations in OCaml by composing stateful differential operators, which we have extracted from Rocq.

Bio:    Runqing Xu is a third year PhD student in Karlsruhe Institute of Technology (KIT), Germany. His research interests lie in incremental computing and formal verification. He has published papers at POPL, ECOOP, CADE, and ATVA. Before being a PhD student, he was a master student at Institute of Software, Chinese Academy of Sciences.