Google, IBM & Meta Certificates — All 10,000+ Courses at 40% Off
One annual plan covers every course and certificate on Coursera. 40% off for a limited time.
Get Full Access
This conference talk from CoqPL 2025 presents research on developing a standard library of differential operators for programming complex incremental computations. Explore how Runqing Xu and Sebastian Erdweg formulate a general framework that maps input changes to output changes while leveraging algebraic properties of non-incremental operations to optimize performance. Learn about their implementation in Coq, including their successful verification of existing efficient differential operators and development of new ones. The 23-minute presentation, sponsored by ACM SIGPLAN, was delivered at the CoqPL 2025 workshop on January 25, 2025, as part of the POPL25 conference.
