τ:: = Top | α | ρ | τ
1
→ τ
2
| \A α\leqslant τ
1
. τ
2
e :: = x | λx:τ.e | e
1
e
2
| Λ α\leqslant τ.e | e [ τ]
slide
:
The bounded type calculus