703640 Interactive Theorem Proving
summer semester 2015 | Last update: 10.09.2015 | Place course on memo list703640
Interactive Theorem Proving
VO 2
4
weekly
every 2nd year
English
Students who have completed this module are familiar with the verification of specifications. They know first- and higher-order logics and can carry out structured proofs in those logics and verify them in interactive theorem provers
Design of an LCF prover; formal proofs; structured proofs and proof scripts; higher-order logic: induction, recursive data structures and recursive functions; automation; termination proofs; correctness of programs
Lectures
Written exam
Announced in the course
None
not applicable
Begin as announced
see dates
- Faculty of Mathematics, Computer Science and Physics
|
Group 0
|
||||
|---|---|---|---|---|
| Date | Time | Location | ||
|
Tue 2015-03-03
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-03-10
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-03-17
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-03-24
|
10.15 - 12.00 | rr 22 rr 22 | ||
|
Tue 2015-04-14
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-04-21
|
08.15 - 10.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-04-28
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-05-05
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-05-12
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-05-19
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-05-26
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-06-02
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-06-09
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-06-16
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Tue 2015-06-23
|
10.15 - 12.00 | 3W04 3W04 | Barrier-free | |
|
Fri 2015-09-25
|
13.00 - 16.30 | HSB 9 HSB 9 | Barrier-free | third exam |