- 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." - Proofs in implicational logic; Introduction to lambda calculus;
Introduction to Lego
(dvi file).
Getting started with LEGO is here.

- Adding and, or, and absurd; More about Lego
(dvi file).
- Typing connectives with axiom schemes; introduction
to universal quantification; translating lambda calculus
into S and K combinators.
(dvi file).
- 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.

- Computation revisited. Rules for equality.
(dvi file).
Lego file containing examples of equational proofs.

- Proof by induction.
(dvi file).
- Prop and Type rules; existential quantification.
(dvi file).
- Algorithms for unification and refinement.
(dvi file).
- Sigma types; development of programs with proofs of correctness.
(dvi file).
Lego file containing the development of an integer square root function.

- Defining inductive types; mutually inductive definitions.
(dvi file).
Lego file containing and/or tree definition.

- Inductive families of types.
(dvi file).
- Equality; definitions of logical connectives
(dvi file).
Lego output from example proof discussed in class.

- Abstract Data Types in type theory
(dvi file).
- Reasoning about imperative programs; reasoning about
nonlocal control.
(dvi file).

Judith Underwood