Problem 6 - Typed $\lambda$-calculus

1.

Explain a simply typed $\lambda$-calculus.

2.

What is the strong normalizability of $\lambda$-calculus.

3.

Describe an outline of the proof of strong normalizability of symply typed $\lambda$-calculus.

See [HIN86] for a detailed answer.