These errata represent bugs in the submitted version of the paper.
They have been fixed in the version available for FTP.
Page 5, in the definition of the context C[ ]:
``$K$'' should be defined as the standard combinator $(\lambda x.\lambda y.x)$.
Page 5, just before Theorem 3.2:
The claim that ``the problem of typability for $\Lambda_k$ easily reduces
to the problem for $\Lambda_{k+1}$'' is wrong. This should read instead
that ``the same analysis for $\Lambda_3$ can be repeated for each
$\Lambda_k$ for $k\geq 4$''.
Page 8, in Lemma 5.2:
The abstractions in the $\lambda$-term $M$ should be labelled.
Specifically, each occurrence of $\lambda x_i$ should be replaced by
$\lambda^2 x_i$ and each occurrence of $\lambda y_i$ should be replaced by
$\lambda^1 y_i$.
page 8, just after Lemma 5.2:
In the example given of an ML equivalent to $M$, the sequence of
$\lambda$-bindings at the beginning should be replaced by:
fn x_1 => fn x_2 => ... => fn x_m =>
Section 5:
A lemma should be added to point out that there are no nonadjacent
companions in a $\theta$-normal form, i.e. all 1-labelled abstractions
belong to $\beta$-redexes.
Page 9, in Figure 4:
The rule $\text{APP}^{\theta,+}$ should be replaced by the rule LET:
\[
{A\cup\{x:\forall.\sigma\} \vdash M : \tau,
\qquad
A \vdash N : \sigma
\over
A \vdash ((\lambda^1 x.M)N) : \tau}
\hskip 1cm
\sigma,\tau\in S(0)
\]
In ASCII form where ``V'' and ``\'' mean $\forall$ and $\lambda$:
A + { x : V.s } |- M : \tau, A |- N : s
----------------------------------------- s,t in S(0)
A |- ((\^1 x.M)N) : t
Page 9, in Figure 4:
The side condition of the rule $\text{ABS}^{\theta,2}$ is incorrect and
should be removed.
Page 11, in the depiction of the form of $M$:
The abstractions in the $\lambda$-term $M$ should be labelled.
Specifically, each occurrence of $\lambda x_i$ should be replaced by
$\lambda^2 x_i$ and each occurrence of $\lambda y_i$ should be replaced by
$\lambda^1 y_i$.
Page 11, in the middle of the page:
The definition of $\tau \doteq \mu$ should mention that $\alpha$ is
required to be a fresh variable, mentioned in no other inequality.