logical verification 2010

logical verification 2010 - 2011

Extra exam

For those who already finished the practical work, an extra exam is scheduled on January 18, 2012. Please consult the schedules for a check and the details.

Schedule 2010-2011

The course is taught in period 5.
The lectures are on Tuesdays 13.30-15.15 and on Fridays 13.30-15.15.
The practical works are on Thursdays 09.00-10.45 and on Fridays 09.00-10.45.
Lecturer: Femke van Raamsdonk
For 2011-2012: if you are interested in this course, please contact femke at cs.vu.nl.

Lectures and practical works 2010-2011

week	lectures	practical works
13	Tuesday March 29, 13.30-15.15, room F637
	lecture 1 4-up b
		Thursday March 31, 09.00-10.45, room P323
		practical work 1
		Friday April 1, 09.00-10.45, room P323
		practical work 2
	Friday April 1, 13.30-15.15, room F654
	lecture 2 4-up b
14	Tuesday April 5, 13.30-15.15, room F637
	lecture 3 4-up b
		Thursday April 7, 09.00-10.45, room P323
		practical work 3
		Friday April 8
		no practical work symposium logic and culture
	Friday April 8
	no lecture symposium logic and culture
15		Monday April 11: deadline prac01.v
	Tuesday April 12, 13.30-15.15, room F637
	lecture 4 4-up b
		Thursday April 14, 09.00-10.45, room P323
		practical work 4
		Friday April 15, 09.00-10.45, room P323
		practical work 5
	Friday April 15, 13.30-15.15, room F654
	lecture 5 4-up b
16	Tuesday April 19, 13.30-15.15, room F637
	lecture 6 4-up b
		Wednesday April 20: deadline prac02.v
		Thursday April 21
		practical work 6
		Friday April 22
		no practical work (Good Friday)
	Friday April 22
	no lecture (Good Friday)
17	Tuesday April 26, 13.30-15.15, room F637
	lecture 7 4-up b
		Thursday April 28, 09.00-10.45, room P323
		practical work 7
		also Thursday April 28: deadline prac03.v
		Friday April 29, 09.00-10.45, room P323
		practical work 8
	Friday April 29, 13.30-15.15, room F654
	lecture 8 4-up b
18	Tuesday May 3, 13.30-15.15, room F637
	lecture 9 4-up b
		Thursday May 5
		no practical work
		Friday May 6
		no practical work
	Friday May 6
	no lecture
19	Tuesday May 10, 13.30-15.15, room F637
	lecture 10 4-up b
		Wednesday May 11: deadline prac04.v
		Thursday May 12, 09.00-10.45, room P323
		practical work 9
		Friday May 13, 09.00-10.45, room P323
		practical work 10
	Friday May 13, 13.30-15.15, room F654
	lecture 11 4-up b
20	Tuesday May 17, 13.30-15.15, room F637
	lecture 12 4-up b
		Wednesday May 18: deadline prac05.v
		Thursday May 19, 09.00-10.45, room P323
		practical work 11
		Friday May 20, 09.00-10.45, room S345 (!)
		practical work 12
	Friday May 20, 13.30-15.15, room F654
	question hour 4-up b
21	Friday May 27, 12.00-14.45, room D107	Friday May 27: deadline recap.v
	exam

Lectures: material and info

Slides: are or will be available via links in the schedule above.
Course notes: preliminary version.
Exercises:
on propositional logic and simply typed lambda-calculus and also the version with answers
on inductive definitions and also the version with answers
on predicate logic and dependent types and also the version with answers
on prop2 and polymorphic types and also the version with answers

Practical works: material and info

The files for the practical work are available via ProofWeb.
The files prac01.v, prac02.v, prac03.v, prac04.v, prac05.v form the obligatory part of the practical work. If you have a pass for all 5 files, then you have a pass for the complete practical work part of the course.
Please send an email to femke at cs.vu.nl if you have a problem with the schedule, the deadlines, or the contents of the practical work !

Bonus Coq Assignment

The file recap.v is the bonus Coq assignment. The file is available via ProofWeb. For this you can obtain at most 0.5 extra on your exam degree (for a total of at most 10).
Note that the final degree is of the form 7 or 7.5 etcetera (but no 5.5). Example: 6.3 for the exam, 0.4 bonus, yields 6.6 yields final degree 6.5. Example: 9.8 for the exam, 0.3 bonus, yields 10.1, final degree 10.

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 in 6 files on the proofweb server which is located at the Radboud University Nijmegen.

See also the description in the studyguide.

Useful links

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

The question hour is in week 20: Friday May 20, 13.30--15.15 in room F654.
The (written) examination for 2010-2011 is in week 21: Friday May 27, 12.00--14.45 in room D107.
(Please check this!)
The resit for 2010-2011 is in week 34: Monday August 22, 12.00--14.45 in room M129.
(Please check this!)
In order to participate you need to have passed the practical work.
Some old exams can be found here.

Questions ?

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

Last update August 31, 2011.