\begin{frame}
  \frametitle{ILPO\ldots Historical overview}
  
  Kamin and L\'evy [1980] (lexicographic path order, LPO):
  \begin{itemize}
    \item Kruskal's Tree Theorem was used in the original proofs
    \item Buchholz [1995] simplified the proof: Kruskal not needed
  \end{itemize}
  
  Bergsta and Klop [1985]:
  \begin{itemize}
    \item Iterative version of RPO: `star method'
    \item Operational definition of reduction order\\ via an auxiliary term rewriting system (with stars)
  \end{itemize}
  
  Klop, van Oostrom and de Vrijer [2005]:
  \begin{itemize}
    \item Extension of the star method to LPO
    \item \emph{Iterative lexicographic path order (ILPO)}
  \end{itemize}
  
\end{frame}