Computer Verified Exact Analysis (Tutorial)

Bas Spitters & Russell O'Connor
This tutorial will illustrate how to use the Coq proof assistant to implement effective and provably correct computation for analysis. Coq provides a dependently typed functional programming language that allows users to specify both programs and formal proofs. We will introduce dependent type theory and show how it can be used to develop both mathematics and programming. We will show how to use dependent type theory to implement constructive analysis. Specifically we will cover how...