Computer Verified Exact Analysis

author: Russell O'Connor, Institute of Computing and Information Sciences, Radboud University Nijmegen
author: Bas Spitters, Institute of Computing and Information Sciences, Radboud University Nijmegen

Description

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. Attendees are encouraged to download and install Coq 8.2 from http://coq.inria.fr/download and also download and make the full system of C-CoRN from http://c-corn.cs.ru.nl/download.html beforehand.

You might be experiencing some problems with Your Video player.

*Slides*
0:00	Tutorial: Computer veried implementation of analysis
0:10	Meeting in Nijmegen
0:27	Outline
1:38	Computing with real numbers - 1
2:22	Computing with real numbers - 2
2:58	Computing with real numbers - 3
3:07	Computing with real numbers - 4
3:30	Computing with real numbers - 5
4:16	Exact analysis
5:42	Computational framework
6:39	Motivation - 1
7:40	Motivation - 2
8:00	Motivation - 3
8:23	Motivation - 4
9:58	Motivation - 5
10:17	Proof assistant - 1
11:06	Proof assistant - 2
12:54	Proof assistants - 1
14:12	Proof assistants - 2
14:21	Proof assistants - 3
14:43	Proof assistants - 4
16:12	Proof assistants - 5
16:27	Proof assistants - 6
19:02	Motivation - 6
19:12	Types - 1
20:00	Types - 2
20:44	Types - 3
22:01	Types - 4
22:06	Types - 3
22:12	Types - 4
22:24	Types - 3
22:31	Types - 4
23:18	Curry-Howard-deBruijn isomorphism
24:32	Computational framework
25:32	Reals - 1
28:12	Constructive logic - 1
28:55	Constructive logic - 2
30:22	Reals - 2
31:01	Reals - 3
31:41	Reals - 4
31:52	Functional programming - 1
33:22	Functional programming - 2
34:42	Functional programming - 3
35:00	Monads - 1
36:00	Monads - 2
36:58	Monads - 3
37:43	Monads in Haskell - 1
37:51	Monads in Haskell - 2
38:22	Monads in Haskell - 3
38:31	Monads in Haskell - 4
38:58	Monads in Haskell - 5
39:16	Monads in Haskell - 6
39:40	Monads - 4
41:36	Monads - 5
42:38	O'Connor completion monad - 1
45:50	O'Connor completion monad - 2
47:30	Motivation - 7
48:41	Motivation - 8
49:00	Brief history of Bishop program in type theory
50:58	Real world programs - 1
51:49	Real world programs - 2
51:51	Real world programs - 3
53:18	References

Lecture rating

People found this lecture:
Worth seeing
because it is:
Valuable and informative
Well presented
Easily understandable
Acceptably recorded
You need to login to cast your vote.

Report a problem or upload files

If you have found a problem with this lecture or would like to send us extra material, articles, exercises, etc., please use our ticket system to describe your request and upload the data.
Enter your e-mail into the 'Cc' field, and we will keep you updated with your request's status.