Logical Verification 2014-2015

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 2014-2015

The course is taught in period 5.
Monday 09.00-10.45: practical work in P323
Monday 11.00-12.45: lecture in S655
Thursday 09.00-10.45: practical work in P323
Thursday 11.00-12.45: lecture in M639
See also the course schedule.

teacher: Femke van Raamsdonk

The remainder of this website contains information about the course in 2012-2013.

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: f.van.raamsdonk at vu.nl).
Last update March 2, 2015.