Overview
AI, Data Science & Cloud Certificates from Google, IBM & Meta — 40% Off
One plan covers every Professional Certificate on Coursera. 40% off Coursera Plus Annual.
Unlock All Certificates
Watch a 22-minute conference talk from CoqPL 2025 that explores the development of a framework for verifying numerical algorithm variants. Presented by researchers from Harvey Mudd College and Lawrence Livermore National Laboratory, this talk addresses the challenge of ensuring correctness in reimplemented classical numerical algorithms amid the evolving landscape of scientific computing. Learn about their preliminary work using the Gram-Schmidt orthogonalization process as a case study, demonstrating how to verify a numerically stable variant (Modified Gram-Schmidt) through exact Real equivalence with its classical counterpart. The presentation was delivered at the ACM SIGPLAN-sponsored CoqPL 2025 workshop on January 25, 2025.
Syllabus
[CoqPL'25] Towards Verified Linear Algebra Programs Through Equivalence
Taught by
ACM SIGPLAN