--- /dev/null
+# System F and recursive types
+
+In the simply-typed lambda calculus, we write types like <code>σ
+-> τ</code>. This looks like logical implication. Let's take
+that resemblance seriously. Then note that types respect modus
+ponens: given two expressions <code>fn:(σ -> τ)</code> and
+<code>arg:σ</code>, the application of `fn` to `arg` has type
+<code>(fn arg):τ</code>.
+
+Here and below, writing <code>x:α</code> means that a term `x`
+is an expression with type <code>α</code>.
+
+This is a special case of a general pattern that falls under the
+umbrella of the Curry-Howard correspondence. We'll discuss
+Curry-Howard in some detail later.
+
+System F is due (independently) to Girard and Reynolds.
+It enhances the simply-typed lambda calculus with quantification over
+types. In System F, you can say things like
+
+<code>Γ α (\x.x):(α -> α)</code>
+
+This says that the identity function maps arguments of type α to
+results of type α, for any choice of α. So the Γ is
+a universal quantifier over types.
+
+