\documentclass{rtaloop}
\rtalabel{explicit-substitution}

\begin{document}
\begin{solvedproblem}{Pierre Lescanne}{}{April 1995}

\begin{abstract}
  Is there a calculus of explicit substitution that is both confluent
  and preserves termination?
\end{abstract}
There are confluent calculi of explicit substitutions, but these do
not preserve termination (strong normalization)
\cite{CurienHardinLevy92,Mellies95}, and there are calculi that are
not confluent on open terms, but which do preserve termination
\cite{LescanneR94}. Is there a calculus of explicit substitution that
is both confluent and preserves termination?

\begin{remark}
  The calculus presented in \cite{Munioz:lics96} enjoys both properties. This
  has led to \rtaref{explicit-substitution-all}.
\end{remark}

\end{solvedproblem}

\end{document}