-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
-give rise to the question of what sort of computation classical logic
-corresponds to---as we'll see later, the answer involves continuations.
+The Curry-Howard correspondence 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.