added Curry-Howard

[lambda.git] / week6.mdwn

diff --git a/week6.mdwn b/week6.mdwn
index 79b12f7..5f225d3 100644 (file)
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -174,7 +174,7 @@ execution.  In Scheme parlance, functions on the unit type are called
 Curry-Howard, take 1
 --------------------
 
-We will returnto the Curry-Howard correspondence a number of times
+We will return to 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
@@ -186,9 +186,9 @@ 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 `σ --> τ`.
+the abstract `\xM` has type σ `-->` τ.
 
-If a term `M` has type `σ --> &tau`, and a term `N` 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