\documentclass{rtaloop}
\rtalabel{typability}

\begin{document}
\begin{solvedproblem}{}{}{April 1991}

\begin{abstract}
Is it decidable whether a term is is typable in the second-order $\lambda 2$
calculus? 
\end{abstract}

One of the outstanding open problems in typed lambda calculi is the following:
Given a term in ordinary untyped lambda calculus, is it decidable whether it
can be typed in the second-order $\lambda 2$ calculus? See
\cite{B91:hlcs}\cite{H90:aw}.


\begin{remark}
This question has been solved in the negative. In \cite{W94:lics} J.B. Wells
proves
that given a closed, type-free lambda term, the question whether it is
typable in second-order $\lambda 2$ calculus, is undecidable. Moreover,
given a closed type-free lambda term $M$ and a type $\sigma$,
then it is also undecidable in
second-order $\lambda 2$ calculus whether $M$ has type $\sigma$.
\end{remark}

\end{solvedproblem}
\end{document}