Next: Exercises
Up: Computer Aided Formal Reasoning
Previous:
Further information about the LEGO system
Lecture notes
- Programming with recursion operators.
(dvi file)
- Deriving programs using refinement.
(dvi file)
- Propositional logic I
(dvi file)
- Propositional logic II
(dvi file)
- Universal quantification and defining logical connectives
(dvi file)
- Existential quantification and equality
(dvi file)
- Induction
(dvi file)
- Unification and Refinement
(dvi file)
- Quantification -- Sigma and Pi types
(dvi file)
- Inductive definitions
(dvi file)
(Lego file with examples)
- Families of inductive types -- vectors and finite sets
(dvi file)
- Equality
(dvi file)
- Abstract Data Types I
(dvi file)
- Abstract Data Types II and Specification
(dvi file)
- Extended Calculus of Constructions and Pure Type Systems
(dvi file)
- Call/cc as a classical operator
(dvi file)
Thomas Schreiber