CS_336/CS_M36 (second part)/CS_M46 Interactive Theorem proving
Lent Term 2006
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 J
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.
- Section 4: The lambda-calculus with products and conjunction
- Section 5: The logical framework.
- Section 6: Data types.
- Revision lecture
Other Course Material
- Documentation about Agda
- Module given in previous years
Last modified: Wed Mar 14 18:49:05 GMT 2007