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

Detailed schedule 2014-2015

week day what slides deadline
14 mon 30 no practical work - -
mon 30 lecture 1 slides -
thu 2 practical work 1 - ???
thu 2 lecture 2 slides -
15 mon 6 NO PRACTICAL WORK - -
mon 6 NO COURSE - -
thu 9 practical work 2 - -
thu 9 lecture 3 slides -
16 mon 13 practical work 3 - -
mon 13 lecture 4 slides -
thu 16 practical work 4 - -
thu 16 lecture 5 slides -
17 mon 20 practical work 5 - -
mon 20 lecture 6 slides -
thu 23 practical work 6 - -
thu 23 lecture 7 slides -
18 mon 27 NO PRACTICAL WORK - -
mon 27 NO LECTURE - -
thu 30 practical work 7 - -
thu 30 lecture 8 slides -
19 mon 4 practical work 8 - -
mon 4 lecture 9 slides -
thu 7 practical work 9 - -
thu 7 lecture 10 slides -
20 mon 11 practical work 10 - -
mon 11 lecture 11 slides -
thu 14 NO PRACTICAL WORK - -
thu 14 NO LECTURE - -
21 mon 18 practical work 11 - -
mon 18 lecture 12 slides -
thu 21 NO PRACTICAL WORK - -
thu 21 question hour -
22 wed 27 EXAM - -
28 thu 9 RESIT - -

Material and info

Useful links

Exam

Questions ?

Send an email to Femke (e: f.van.raamsdonk at vu.nl).
Last update March 23, 2015.