logical verification 2009

logical verification 2009 - 2010

This year (2009-2010)

In 2009-2010 logical verification will be taught in the periods 5 and 6 (earlier announcements said 4 and 5). The information below is about the course from 2008-2009. It will be updated for the version of 2009-2010.

Contents of the course (2008-2009)

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.

See also the description in the studyguide.

Course (2008-2009)

weeks 37(!)-42: Friday 13.30 - 15.15 in F640
weeks 44-50: Friday 11.00 - 12.45 in C121

NB: we start one week later than announced on the FEW schedule, because of the

Symposium in honour of N.G. de Bruijn at the TU/e Eindhoven on Friday September 5, 2008.

Practical work (2008-2009)

weeks 38-42 and 44-50: Thursday 11.00 - 12.45 in S345.
(NB: the practical work starts in week 38, following the first course in week 37.)

See also the FEW schedule.

Lecturers

Femke van Raamsdonk, e: femke at cs.vu.nl.

Course material (2008-2009)

The material for the lectures and the practical work can be found here.

Practical work (2008-2009)

The practical work is concerned with the proof checker Coq. Using a web interface we will work on a server at the Radboud University Nijmegen. The files containing the exercises will be availble on this server (and also via the homepage of the course). The Coq exercises are made during the practical work. Everyone should hand in his/her solution individually, but of course it is ok (even recommended) to discuss your work with others. The deadline for handing in the exercises is the next Tuesday (five days after the practical work) at 12.00. The exercises are graded "pass" or "fail". In order to participate in the examination 9 out of 12 must be graded "pass".

Useful links (2008-2009)

The home page of the Coq project with among other things a tutorial and a manual.
The home page of ProofWeb, the web interface developed in the project ProofWeb (Surf Foundation, Radboud University Nijmegen, Vrije Universiteit Amsterdam).
The home page of Caml.
The home page of Proof General (another interface for Coq).

Exam (2008-2009)

The (written) examination was on Thursday December 18, 2008, 08.45-11.30 in M143.
The resit is on Monday February 16, 18.30-21.15, in Q105.
Please check this!
In order to participate you need to have passed the practical work, which is the case if 9 out of 12 homework assignments are graded "pass".
Some exercises with answers and some old exams can be found here.

Questions ?

Send an email to Femke (e: femke at cs.vu.nl).

Last update August 20, 2009.