Lecture notes

1. Introduction to constructive logic (dvi file).

   Correction to notes distributed in class: page 4, third paragraph, second sentence should read "Since there are no formulas to the left of the turnstile, this gives us a proof of P->P from no assumptions, which means that P->P is a theorem of the system."

2. Proofs in implicational logic; Introduction to lambda calculus; Introduction to Lego (dvi file).

   Getting started with LEGO is here.

3. Adding and, or, and absurd; More about Lego (dvi file).

4. Typing connectives with axiom schemes; introduction to universal quantification; translating lambda calculus into S and K combinators. (dvi file).

5. Data types: bool, nat, list. Defining functions. (dvi file). Contains new, improved (i.e. correct) description of the reduction of 2+2!

   Here is an annotated description of the reduction of 5+2.

6. Computation revisited. Rules for equality. (dvi file).

   Lego file containing examples of equational proofs.

7. Proof by induction. (dvi file).

8. Prop and Type rules; existential quantification. (dvi file).

9. Algorithms for unification and refinement. (dvi file).

10. Sigma types; development of programs with proofs of correctness. (dvi file).

    Lego file containing the development of an integer square root function.

11. Defining inductive types; mutually inductive definitions. (dvi file).

    Lego file containing and/or tree definition.

12. Inductive families of types. (dvi file).

13. Equality; definitions of logical connectives (dvi file).

    Lego output from example proof discussed in class.

14. Abstract Data Types in type theory (dvi file).

    Lego file of examples.

15. Reasoning about imperative programs; reasoning about nonlocal control. (dvi file).