Logical Verification 2016–2017

Contents of the course

A proof assistant is a program that checks the correctness of a specification of a program, or the proof of a theorem. In the practical work of the course, we use the proof assistant Coq, which is based on a typed lambda-calculus. The theoretic part of the course is concerned with type theory and the correspondence between logic and typed lambda-calculi called the Curry–Howard–De Bruijn correspondence. We study various typed lambda-calculi and the corresponding logics.

During the practical works, we do Coq exercises. They are available on the ProofWeb server at Radboud University Nijmegen.

See also the description in the study guide.

Schedule 2016–2017

The course is taught in period 5. We have lectures on Mondays and on Thursdays, and practical work on Tuesdays and on Fridays. See also the course schedule.

Lecturer: Jasmin Christian Blanchette

Detailed schedule 2016–2017

week day we do
14 Mon 3 Apr lecture 1
slides 4-up 1-up
Tue 4 Apr practical work 1
Thu 6 Apr lecture 2
slides 4-up 1-up
Fri 7 Apr practical work 2
15 Mon 10 Apr lecture 3
slides 4-up 1-up
Tue 11 Apr practical work 3
16 Thu 20 Apr lecture 4
slides 4-up 1-up
Fri 21 Apr practical work 4
17 Mon 24 Apr lecture 5
slides 4-up 1-up
Tue 25 Apr practical work 5
18 Mon 1 May lecture 6
slides 4-up 1-up
Tue 2 May practical work 6
Thu 4 May lecture 7
slides 4-up 1-up
19 Mon 8 May lecture 8
slides 4-up 1-up
Tue 9 May practical work 7
Thu 11 May lecture 9
slides 4-up 1-up
Fri 12 May practical work 8
20 Mon 15 May lecture 10
slides 4-up 1-up
Tue 16 May practical work 9
Thu 18 May lecture 11
slides 4-up 1-up
Fri 19 May practical work 10
21 Mon 22 May lecture 12
slides 4-up 1-up

Deadlines for the practical works 2016–2017


Useful links



Send an email to j.c.blanchette shtrudel vu.nl.