\documentclass{rtaloop}
\rtalabel{strong-normalization}


\begin{document}
\begin{problem}{Jean-Jacques L\'evy}{}{April 1991}

\begin{abstract}
  Can strong normalization of the typed lambda calculus be proved by a
  reasonably straightforward mapping from typed terms to a well-founded
  ordering?
\end{abstract}
  
  Can strong normalization (termination) of the typed lambda calculus
  be proved by a reasonably straightforward mapping from typed terms
  to a well-founded ordering?  Note that the type structure can remain
  unchanged by $\beta$-reduction.  The same question arises with
  polymorphic (second-order) lambda calculus.

\end{problem}
\end{document}