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

(to be updated)
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

Deadlines for the practical works 2016–2017


Useful links



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