Critical Systems (CS_411, Academic Year 2002/03)

Lent Term 2003

Lecturer

Dr. A. Setzer
Dept. of Computer Science
University of Wales Swansea
Singleton Park
Swansea
SA2 8PP,UK
Tel. (01792) 513368
Fax (01792) 295651

Timetable

Thursday, 10:00, Robert Recorde Room
Friday, 12:00, Robert Recorde Room

Slides, Handouts

These slides are presented only for access by my students (I haven't figured out yet how to restrict the access). Please refer to the copyright notice on slide 7 of Section 1.
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.

Slides

Agda examples used in the lectures are available from
- here
Section A0:
- Pdf
- Postscript
Section A1:
- Pdf
Section A2:
- Pdf
Section A3:
- Pdf
Section B1:
- Pdf
Section B2:
- Pdf
Section B3 (unfinished yet):
- Pdf
Revision Lecture:
- Pdf

Other Course Material

Agda
- Installation of Agda
- Creating Latex output from Agda files
- Agda reference card
  - pdf
  - postscript
- Getting started with Agda.
  - pdf
  - postscript
Literature
- Book: Programming in Martin-Löf's Type Theory
- B. Nordström, K. Petersson, J. Smith: Martin-Löf's Type Theory. In: Handbook of Logic in Computer Science. Oxford University Press, 2000.
- For viewing and printing those files, you need to be able to view postscript files. This can be done in the Linux lab. Download the file, execute from a shell "gunzip file.ps.gz" and then "ghostview file.ps", where file is the name of your file.