How to Prove a Calculation Correct? - IPAM at UCLA

Offered By: Institute for Pure & Applied Mathematics (IPAM) via YouTube

Course Description

Overview

Explore an alternative approach to proving calculations correct in this 52-minute conference talk by James Davenport from the University of Bath. Delve into the challenges of proving algorithm and implementation correctness, and discover a method where the implementation produces intermediate information during calculations. Learn how this information can be used by proof engines to construct proofs of correctness for specific calculations, rather than general algorithms. Examine this methodology in the context of real algebraic geometry, also known as NRA in SMT-language. Gain insights into advanced mathematical concepts and their applications in machine-assisted proofs, presented at IPAM's Machine Assisted Proofs Workshop at UCLA.

Syllabus

James Davenport - How to prove a calculation correct? - IPAM at UCLA

Taught by

Institute for Pure & Applied Mathematics (IPAM)

Related Courses

Certificates of Nonnegativity and Their Applications in Theoretical Computer Science
Society for Industrial and Applied Mathematics via YouTube Hilbert's 16th Problem and O-Minimality - Lecture 1
Fields Institute via YouTube Global Optimization via the Dual SONC Cone and Linear Programming
Fields Institute via YouTube Techniques of Resolution of Singularities in Quasianalytic Classes - Lecture 1
Fields Institute via YouTube Polynomial Time Guarantees for the Burer-Monteiro Method
Fields Institute via YouTube