-Curry-Howard, take 1
---------------------
-
-We will returnto the Curry-Howard correspondence a number of times
-during this course. It expresses a deep connection between logic,
-types, and computation. Today we'll discuss how the simply-typed
-lambda calculus corresponds to intuitionistic logic. This naturally
-give rise to the question of what sort of computation classical logic
-corresponds to---as we'll see later, the answer involves continuations.
-
-So at this point we have the simply-typed lambda calculus: a set of
-ground types, a set of functional types, and some typing rules, given
-roughly as follows:
-
-If a variable `x` has type σ and term `M` has type τ, then
-the abstract `\xM` has type `σ --> τ`.
-
-If a term `M` has type `σ --> &tau`, and a term `N` has type
-σ, then the application `MN` has type τ.
-
-These rules are clearly obverses of one another: the functional types
-that abstract builds up are taken apart by application.
-
-The next step in making sense out of the Curry-Howard corresponence is
-to present a logic. It will be a part of intuitionistic logic. We'll
-start with the implicational fragment (that is, the part of
-intuitionistic logic that only involves axioms and implications):
-
-<pre>
-Axiom: ---------
- A |- A
-
-Structural Rules:
-
-Exchange: Γ, A, B, Δ |- C
- ---------------------------
- $Gamma;, B, A, Δ |- C