Scale By the Bay 2021 intro video by Ryan Orendorff
summary
Claims that functional programming plus dependent types yields verified linear algebra by representing matrices as matrix-free functions between vector spaces and proving core identities in Agda. Shows implementation of matrix-free optimization algorithms and a proof that the function-based code matches conventional matrix implementations, while reporting comparable space and time performance. Finishes with a concrete comparison to implementations in Python and dependently typed Haskell to expose trade-offs of added formalism.
AI-written summary · about
related talks
50mUsing Dependent Types in Mathematical Optimization Algorithms
01h 18mC++ and Linear Algebra
05mDBTB INT Marek Kolodziej r
22mTowards Verified Linear Algebra Programs Through Equivalence
49mIntroduction to Linear Type Systems and Linear Haskell
48mEnhancing your Haskell with Dependently Typed Programming
35mA Crash Course in Applied Linear Algebra
58mFunctional Array Funhouse Intensive - Part 2 of 5