CS_336/CS_M36 (second part) Interactive Theorem proving

Lent Term 2005

Lecturer

Timetable

• Tuesday, 12:00, Glyndwr Building, Room A
• Thursday, 13:00, Glyndwr Building, Keir Hardie Builiding, Room 250

Slides, Handouts

• 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.
• Slides by section
  • Errata
    • Postscript (gzipped)
    • Pdf
  • Section 0
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version (gzipped) with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version (gzipped) with 4 slides per page -- suitable for printing
  • Section 1
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version (gzipped) with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version (gzipped) with 4 slides per page -- suitable for printing
  • Section 2
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version (gzipped) with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version (gzipped) with 4 slides per page -- suitable for printing
  • Section 3
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version (gzipped) with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version (gzipped) with 4 slides per page -- suitable for printing
  • Section 4
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version (gzipped) with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version (gzipped) with 4 slides per page -- suitable for printing

Other Course Material

• Agda
  • Examples used in the lecture
  • Installation of Agda
  • Creating Latex output from Agda files
  • Agda reference card
    • pdf
    • postscript (gzipped)
  • Getting started with Agda.
    • pdf
    • postscript (gzipped)
• Documentation about Agda
  • >Some Tutorial on Agda (under preparation; only latex source fiels available).
    • Pdf file created from the above mentioned sources (for the most recent version refer to the latex sources).
• XEmacs/Emacs
  • XEmacs Reference Card
  • Reference card Emacs
  • Reference card Emacs from Indiana University
• 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.

Links

• Module given in previous years
  • Course page Interactive Theorem Proving from 2003/04
  • Course page Critical Systems CS_411 from 2002/03 (Stream B relevant for this module)
  • Course page Critical Systems CS_411 from 2001/02 (Stream B relevant for this module)