CS_336/CS_M36 (second part)/CS_M46 Interactive Theorem proving

Lent Term 2008

Lecturer

Timetable

• Tuesday, 12:00, Faraday B
• Thursday, 12:00, Faraday C

Coursework

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.
• 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 (Nothing added yet)
  • Errata
    • Postscript
    • Pdf
  • Section 0: Introduction.
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 1: From simple to dependent types.
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 2: Reduction systems and term rewriting.
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 3: The lambda-calculus and implication (includes a basic introduction into Agda).
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 4: The lambda-calculus with products and conjunction
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 5: The logical framework.
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing
  • Section 6: Data types.
    • pdf Version with one page per slide -- unsuitable for printing
    • Postscript Version with one page per slide -- unsuitable for printing
    • pdf Version with 4 slides per page -- suitable for printing
    • Postscript Version with 4 slides per page -- suitable for printing

Other Course Material

• Agda
  • Material developed by Anton Setzer
    • Examples used in the lecture
    • Installation of Agda2
    • List of leim symbols under Agda
    • Use of the abbreviation mode, which makes typing in special symbols much easier
    • Agda reference card (refers still to Agda1)
      • pdf
      • postscript
    • Getting started with Agda (refers still to Agda1).
      • pdf
      • postscript
  • Material from other places
    • A tutorial on Agda
    • Agda (Wikipedia)
    • Agda home page (covers mainly Agda1 at present)
    • Agda Wiki (contains some documentation, downloads; note that Version 2.1.2 doesn't have the coverage and termination checker, which is required for the coursework in the module Interactive Theorem Proving).
    • Documentation about Agda (from the Agda Wiki)
• Alfa
  • Alfa main page (doesn't seem to support the new syntax of Agda or Agda2)
• XEmacs/Emacs
  • XEmacs Reference Card
  • Reference card Emacs
• 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.

Links

• Module given in previous years
  • Course page Interactive Theorem Proving from 2006/07
  • Course page Interactive Theorem Proving from 2005/06
  • Course page Interactive Theorem Proving from 2004/05
  • 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)