Interactive Theorem Proving for Agda Users

• Examples used in the lecture
• Section 0: Introduction
• Section 1: From simple to dependent types.
  • Section 1 (b) summarizes the history of Agda
• Section 2: Reduction systems and term rewriting.
  • Section 2 (a) gives a brief intoduction on getting started with Agda
• Section 3: The lambda-calculus and implication (includes a basic introduction into Agda)
  • Section 3 (c) shows how to formalise the simple lambda calculus in Agda.
  • Section 3 (d) explains the basics of how logic is represented in type theory and therefore as well in Agda (contains no Agda code).
  • Section 3 (e) shows how to carry out proofs in implicational logic in Agda.
• Section 4: The lambda-calculus with products and conjunction
  • Section 4 (c) introduces how to formalised the simply typed lambda calculus with products in Agda.
  • Section 4 (d) introduces logic with implication and conjunction in Agda.
  • Section 4 (g) introduces finite sets, Booleans and decidable formulae in Agda.
• Section 5: The logical framework.
  • Section 5 (e) (from Slide titled "The Dep. Function Set in Agda) introduces the dependent function set and proofs using universal quantifiers in Agda.
  • Section 5 (f) (from Slide titled "The Dependent Product in Agda) introduces the dependent product and proofs using existential quantifiers in Agda. It contains as well simple proofs using equality.
  • Section 5 (i) introduces Set vs. Type in type theory. There is one slide with title Set vs. Type in Agda which links this to Agda.
• Section 6: Data types.
  • Section 6 (c) contains a toy example of verifying the correctness of a program controlling traffic lights in Agda.
  • Section 6 (d) (starting with Disjoint Union in Agda) introduces the disjoint union and disjunction in Agda
  • Section 6 (e) (starting with The Sigma Set in Agda) introduces the Sigma set in Agda
  • Section 6 (f) (from Construct. (or Intuit.) Logic) discusses the logic (constructive logic) used in Agda (no Agda code used).
  • Section 6 (g) (from Natural Numbers in Agda) introduces the natural numbers in Agda.
  • Section 6 (h) introduces Lists in Agda.
  • Section 6 (i) (from Universes in Agda) introduces Universes in Agda.
  • Section 6 (j) introduces briefly data in a more general context.
• Other material
  • The Agda Wiki
    • Installation instructions
  • Installation of Agda2 by Anton Setzer (Some other material is in the old installation pages)
  • Agda (Wikipedia)
  • Agda home page from Japan (covers mainly Agda1 at present)
  • 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 2007/08 (Uses Agda2)
    • Course page Interactive Theorem Proving from 2006/07 (Uses Agda1, new syntax)
    • Course page Interactive Theorem Proving from 2005/06 (Uses Agda1, old syntax)
    • 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)