Type Systems Exercises

Monday 6/24

1. Find the term of the following λ→ types:
   1. (α → β) → (α → α → β)'
   2. ((α → β) → δ) → β → δ
2. Compute the principle type of λx.λy.y x(λz.x)
3. Type λx.xxx in λ2-Curry.
4. Prove that all normal forms are typeable in λ2.
5. Define Sum: List_Nat → Nat that sums the elements of a list.