天基综合信息系统全国重点实验室鲁班青年论坛2026年度第1期

时间：2026年2月27日10:00 – 11:00

地点：中国科学院软件研究所5号楼4层第二会议室
(腾讯会议：967-446-183)

主讲人：Runqing Xu (许润清),Karlsruhe Institute of Technology (KIT) 

报告摘要：

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.

报告人介绍：

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.