Next: Exercises Up: Computer Aided Formal Reasoning Previous: Further information about the LEGO system

Lecture notes

  1. Programming with recursion operators. (dvi file)

  2. Deriving programs using refinement. (dvi file)

  3. Propositional logic I (dvi file)

  4. Propositional logic II (dvi file)

  5. Universal quantification and defining logical connectives (dvi file)

  6. Existential quantification and equality (dvi file)

  7. Induction (dvi file)

  8. Unification and Refinement (dvi file)

  9. Quantification -- Sigma and Pi types (dvi file)

  10. Inductive definitions (dvi file) (Lego file with examples)

  11. Families of inductive types -- vectors and finite sets (dvi file)

  12. Equality (dvi file)

  13. Abstract Data Types I (dvi file)

  14. Abstract Data Types II and Specification (dvi file)

  15. Extended Calculus of Constructions and Pure Type Systems (dvi file)

  16. Call/cc as a classical operator (dvi file)

Thomas Schreiber