703640 Interactive Theorem Proving

winter semester 2016/2017 | Last update: 19.10.2016 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
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