CS_336/CS_M36 (second part)/CS_M46 Interactive Theorem proving
Lent Term 2008
Dr. A. Setzer
of Computer Science
University of Wales Swansea
Tel. (01792) 513368
Fax (01792) 295651
- Tuesday, 12:00, Faraday B
- Thursday, 12:00, Faraday C
In order to reduce plagarism, coursework and solutions to coursework will not
be made available on this website.
- In order to read and print out pdf-files, you need a PDF reader. For instance Acrobat Reader
is available free here:
- For my students: Please don't print these
files on departmental printers.
Instead ask in the student secretary for a copy.
To print out on ordinary printers
costs, because of the cost of the toner,
5 to 10 times more than fotocopying, as done by the lecturer.
- Full Version.
Contains some material which is only available to students taking this course.
(You won't miss much if you don't have access to this version).
Please press the login button.
If your password is not correct, you will be redirected to a non-existing page.
(You might need to enable java script on your browser -
for Internet Explorer see this page for instructions; especially you need to enable "Allow websites to prompt for information using scrpted windows")
Freely accessible version.
- Slides by section
- Section 0: Introduction.
- Section 1: From simple to dependent types.
- Section 2: Reduction systems and term rewriting.
- Section 3: The lambda-calculus and implication (includes a basic introduction into Agda).
- Section 4: The lambda-calculus with products and conjunction
- Section 5: The logical framework.
- Section 6: Data types.
- Old Versions of Sections 3 - 6.
Because of prosper slides no longer being supported,
the above Sections 3 - 6 were converted into latex style beamer in order to carry out some minor corrections.
In case of conversion errors, please refer to the
original slides using latex style prosper:
- Sect. 3 Old
- Sect. 4 Old
- Sect. 5 Old
- Sect. 6 Old
Other Course Material
- Material developed by Anton Setzer
- Material from other places
- Alfa main page (doesn't seem to support the new syntax of Agda or Agda2)
- Module given in previous years
Last modified: Wed Jan 14 14:18:11 GMT 2009