From: Chris Barker
Date: Mon, 25 Oct 2010 02:12:16 +0000 (-0400)
Subject: added Curry-Howard
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=4cc40e4c5ca2646b579213ee40f2caa794a3a474
added Curry-Howard
---
diff --git a/week6.mdwn b/week6.mdwn
index 79b12f71..5f225d36 100644
--- 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