703640 Interactive Theorem Proving

summer semester 2015 | Last update: 10.09.2015 Place course on memo list
703640
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
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