Logical Verification 2014-2015

News

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 P337
Monday 11.00-12.45: lecture in S655
Thursday 11.00-12.45: lecture in M623
Thursday 13.30-15.15: practical work in P337
See also the course schedule.

In addition (not on the course schedule):
Thursday 16.00-17.00: office hour in T446

teacher: Femke van Raamsdonk

Detailed schedule 2014-2015

week day we do
14 mon 30 no practical work
mon 30 lecture 1
prop1
slides 4-up b
thu 2 practical work 1
thu 2 lecture 2
lambda-calculus with simple types
slides 4-up b
15 mon 6 NO PRACTICAL WORK
mon 6 NO COURSE
thu 9 lecture 3
dynamics
slides 4-up b
thu 9 practical work 2
16 mon 13 practical work 3
mon 13 lecture 4
pred1
slides 4-up b
thu 16 lecture 5
lambda-calculus with dependent types
slides 4-up b
thu 16 practical work 4
17 mon 20 practical work 5
mon 20 lecture 6
Curry-Howard and exercises
slides 4-up b
thu 23 lecture 7
inductive datatypes
slides 4-up b
thu 23 practical work 6
18 mon 27 NO PRACTICAL WORK
mon 27 NO LECTURE
thu 30 lecture 8
inductive predicates
slides 4-up b
thu 30 practical work 7
19 mon 4 practical work 8
mon 4 lecture 9
program extraction and exercises
slides 4-up b
thu 7 lecture 10
prop2
slides 4-up b
thu 7 practical work 9
20 mon 11 practical work 10
mon 11 lecture 11
lambda-calculus with polymorphic types
slides 4-up b
thu 14 NO PRACTICAL WORK
thu 14 NO LECTURE
21 mon 18 practical work 11
mon 18 lecture 12
completion
slides 4-up b
thu 21 lecture 13
completion and exercises
slides summary 4-up summary b decidability 4-up decidability b
thu 21 NO PRACTICAL WORK
tue 26 question hour 10.00-11.30 in S624
22 wed 27 EXAM
28 thu 9 RESIT

Deadlines for the practical works (please check again)

Material

Useful links

Exam

Questions ?

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