Meeting Tomorrow

[Joe Razavi]

Hi everyone,

Sorry for taking a long time to send this out. Last week we decided to
have a re-cap session tomorrow; we'll go over chapters 1-4 again
briefly.

I think the key things to understand are:

1) What are lambda terms and beta reduction?
2) What properties of the lambda calculus make it suitable to use as a
programming language?
3) What does a type theory for the lambda calculus do, and why would
we want to use one?
4) Which rules of proof are constructively sound?
5) What do constructive logic and the simply typed lambda calculus
have in common?

Of course, you don't need to bring answers along -- just have these
vaguely in mind :)

If the original link to the reading doesn't work, try this one:
http://www.cs.cmu.edu/~rwh/courses/logic/www/handouts/curry-howard.pdf

See you soon,

Joe