λS: Computable Semantics for Diff'ble Programming with HO Functions and Datatypes

on YouTube ↗30m

" summary

A new differentiable programming semantics, λS, gives computable meanings for higher-order derivatives and for nondifferentiable ops via the Clarke derivative, with primitives for integration, root finding and optimization and an embedded Haskell implementation that computes arbitrary-precision intervals up to a user tolerance. The language represents every function as an infinite derivative tower, evaluates minimization and min01 correctly (derivative converging to −2 in the clearance example), supports differentiable ray tracing and measures, and produces guaranteed interval enclosures rather than floating-point guesses.

AI-written summary · about

" chapters (23)

1. 0:00Intro
2. 0:19Contributions
3. 1:31How to differentiate through...?
4. 3:31As: arbitrary precision
5. 4:10As: libraries for differentiable programming.
6. 5:15Outline of this talk
7. 8:49We can compute higher-order derivatives
8. 9:31A simplified path-planning task
9. 10:19Simple clearance example
10. 11:15An example no preexisting semantics could handle
11. 15:48A first-order semismooth language
12. 16:35First-order functions are streams of kth derivatives
13. 18:20Second-order functions are transformers of first-order functions
14. 19:04integral01 : constructive semantics
15. 21:18Internal first-order functions continuous maps are stream transformers
16. 22:00What is the derivative of ReLU?
17. 23:56Implicit surfaces: example task
18. 25:21We can compute the brightness of the reflected light
19. 25:38A differentiable ray tracer
20. 27:10Generalized parametric surfaces: example task
21. 28:20Minimizers support convex hulls
22. 28:49Probability distributions: example task
23. 29:31Computing mean and variance

" related talks

• 06mDistribution Theoretic Semantics for Non-Smooth Differentiable ProgrammingChristopher Lam · LAFI 2023
• 13mFormalizing a First-order Differentiable Logic with MathCompJairo Miguel Marulanda-Giraldo · RocqPL 2026
• 19mSemantics of Integrating and Differentiating SingularitiesJesse Michel, Hongseok Yang, Wonyeol Lee · PLDI 2025
• 49mSemantic Foundations for Probabilistic ProgrammingChris Heunen · Uncertainty in Computation 2016
• 39mDifferentiable Functional ProgrammingNoel Welsh · Scala Days New York 2018
• 18mA Language and Smoothed Semantics for Convergent Stochastic Gradient DescentC.-H. Luke Ong, Dominik Wagner · LAFI 2022
• 34mDifferentiable Functional ProgrammingNoel Welsh · Scala Days Berlin 2018
• 36mProgramming Languages for Automatic Differentiation: What Now?Damiano Mazza · LAFI 2022