703640 Interactive Theorem Proving
winter semester 2016/2017 | Last update: 19.10.2016 | 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
Begin as announced
see dates
- Faculty of Mathematics, Computer Science and Physics
|
Group 0
|
||||
|---|---|---|---|---|
| Date | Time | Location | ||
|
Fri 2016-10-07
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-10-14
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-10-21
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-10-28
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-11-04
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-11-11
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-11-18
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-11-25
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-12-02
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-12-09
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2016-12-16
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2017-01-13
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2017-01-20
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2017-01-27
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |
|
Fri 2017-02-03
|
12.15 - 14.00 | HSB 9 HSB 9 | Barrier-free | |