Interactive Theorem Proving for Agda Users
This page contains the slides of the module "Interactive Theorem Proving", a third year/postgraduate course held at Swansea University, with a guide to material specifically directed at Agda. The full course page can be found here.
- 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
- Module given in previous years
Last modified: Wed Jan 14 14:20:18 GMT 2009