图 书 馆
计算机验证的精确分析Computer Verified Exact Analysis |
|
| 课程网址: | http://videolectures.net/aug09_spitters_oconnor_cvia/ |
| 主讲教师: | Russell O Connor; Bas Spitters |
| 开课单位: | 拉德布德大学 |
| 开课时间: | 2009-08-24 |
| 课程语种: | 英语 |
| 中文简介: |  |
| 课程简介: | 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 to implement effective real numbers and effective integration. This work will be done using the Coq proof assistant. The tutorial will cover how to use the Coq proof assistant. |
| 关 键 词: | 精确分析; 计算机科学; 逻辑 |
| 课程来源: | 视频讲座网 |
| 最后编审: | 2021-12-23：liyy |
| 阅读次数: | 52 |