This year there are not enough students for the course to be given in the normal way. Students are supposed to watch the video recordings of last year, and the "lectures" on Wednesday will each week be a "responsiecollege".
The proof assistant course consists of three parts:
In this part of the course the Mizar proof assistant is taught from the user perspective. Specific aspects of Mizar are:
The version of Mizar used in the course is Mizar version 7.12.01 (or for Windows).
In this part of the course the HOL Light proof assistant is taught from the implementer perspective. Specific aspects of HOL are:
The version of HOL used in the course is the snapshot of HOL Light of 10th January 2010.
In this part of the course proof assistants different from Mizar, HOL and Coq will be presented.
| Lectures | Wednesday: 13.45-15.30, HG00.308 |
| February 1 | Introduction | LSFA talk QED manifesto | |
| February 8 | Mizar: 1.1-1.3 | clip clip | Mizar intro Mizar manual |
| February 15 | Mizar: 1.4-1.5 | clip clip | Mizar exercise exercise starting point |
| February 22 | no lecture | ||
| February 29 | Mizar: 1.6-1.8 | clip clip | |
| March 7 | Mizar: 2.1-2.3 | clip clip | |
| March 14 | Systems: overview | clip clip | |
| March 21 | HOL: logic | clip clip | HOL manual HOL logic chapter HOL exercise |
| March 28 | HOL: kernel | clip clip | |
| April 4 | quarter break | ||
| April 11 | quarter break | ||
| April 18 | HOL: goals, tactics | clip clip | HOL reference |
| April 25 | HOL: conversions, rewriting | clip clip | |
| May 2 | no lecture | ||
| May 9 | HOL: decision procedures | clip clip | model elimination |
| Systems: presentations | |||
| May 23 | Rob Tiemens: B Method | Presentatie.pdf Aantekeningen.pdf find_nth.tar.gz | |
| June 6 | Roel van Dijk: Agda |
This schedule might be changed if necessary.
Related to the required work of the course there are several dates. Each of the two exercises has a start date, a "halfway point" date, and a deadline. The schedule for this is:
| February 15 | Mizar exercise: handed out |
| March 14 | Mizar exercise: halfway point |
| March 21 | Systems: system for presentation selected |
| March 21 | HOL exercise: handed out |
| April 18 | HOL exercise: halfway point |
| June 20 | Mizar exercise: hard deadline |
| June 20 | HOL exercise: hard deadline |
For each part of the course a grade will be given. The final grade of the course will be the average of those three grades. The first two parts both have an exercise: doing a formalization and implementing a small proof assistant. For the third part a presentation of a proof assistant different from Mizar, HOL and Coq has to be given.