- 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 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
- 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)

Anton Setzer Last modified: Wed Jan 14 14:20:18 GMT 2009