There is a facultative assignment on program verification. This assignment is handed out on the practical session of 9 December 2010. Submission date is 9 January, 2011. A sufficient assignment will add 1 point maximum to the final grade.
The answer to exercise PV 3.1 (Gentzen derivation) of 25 November is presented as an animation. Click on the screen to see the next step. The file is in QuickTime movie format. Let me know if this gives problems.