Logical Verification 2013-2014

The course logical verification is not taught in 2013-2014. If you have questions about the course, please send an email to f.van.raamsdonk @ vu.nl. The remainder of this website contains information about the course in 2012-2013.

Logical Verification 2012-2013

Contents of the course

A proof-assistant is used to check the correctness of a specification of a program, or the proof of a theorem. In the practical work of the course logical verification we use the proof-assistant Coq which is based on typed lambda calculus. The theoretic part of logical verification is concerned with type theory and the correspondence between logic and typed lambda-calculus called the "Curry-Howard-De Bruijn isomorphism". We study various typed lambda calculi and the corresponding logics.
During the practical works we make Coq exercises which are available on the proofweb server which is located at the Radboud University Nijmegen.
See also the description in the study guide.

Schedule 2012-2013

The course is taught in period 5.
The lectures are on Mondays 13.30-15.15 and on Tuesday 13.30-15.15.
The practical works are on Tuesdays 11.00-12.45 and on Fridays 09.00-10.45.
A more detailed schedule is below.
Lecturer: Femke van Raamsdonk

Detailed schedule 2012-2013

week day what slides deadline
14 tue no practical work - -
tue lecture 1 slides 4-up b -
fri no practical work - -
15 mon lecture 2 slides 4-up b -
tue practical work 1 - -
tue lecture 3 slides 4-up b -
fri practical work 2 - -
16 mon lecture 4 slides 4-up b -
deadline prac01.v - -
tue practical work 3 - -
tue lecture 5 slides 4-up b -
fri practical work 4 - -
17 mon lecture 6 slides 4-up b -
deadline prac02.v - -
tue practical work 5 - -
tue lecture 7 slides 4-up b -
fri practical work 6 - -
18 mon no lecture (!) - -
tue no practical work - -
tue no lecture - -
fri practical work 7 - -
19 mon lecture 8 slides 4-up b -
deadline prac03.v - -
tue practical work 8 - -
tue lecture 9 slides 4-up b -
fri no practical work - -
20 mon lecture 10 slides 4-up b -
tue practical work 9 - -
deadline prac04.v - -
tue lecture 11 slides 4-up b -
fri practical work 10 - -
21 mon no lecture - -
tue practical work 11 - -
tue lecture 12 slides 4-up b -
fri practical work 12 - -
deadline prac05.v - -
recap.v is not obligatory - -
22 fri EXAM May 31 - -
28 thu RESIT July 11 - -

Material and info

Useful links

Exam

Questions ?

Send an email to Femke (e: femke at few.vu.nl).
Last update May 21, 2013.