# System F and recursive types
In the simply-typed lambda calculus, we write types like ```
σ
-> τ
```

. This looks like logical implication. Let's take
that resemblance seriously. Then note that types respect modus
ponens: given two expressions `fn:(σ -> τ)`

and
`arg:σ`

, the application of `fn` to `arg` has type
`(fn arg):τ`

.
Here and below, writing `x:α`

means that a term `x`
is an expression with type `α`

.
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
`Γ α (\x.x):(α -> α)`

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.