Computer Verified Exact Analysis
Published on Aug 24, 20098389 Views
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
