\documentclass[10pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{amssymb}
\usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry}
\usepackage{graphicx}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}

\urlstyle{tt}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\renewcommand{\isacharunderscore}{\_}

\begin{document}

\title{Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms}
\author{Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand}

\maketitle

\begin{abstract}
\noindent
This Isabelle/HOL formalization defines recursive path orders (RPOs) for
higher-order terms without $\lambda$-abstraction and proves many useful
properties about them. The main order fully coincides with the standard RPO on
first-order terms also in the presence of currying, distinguishing it from
previous work. An optimized variant is formalized as well. It appears
promising as the basis of a higher-order superposition calculus.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt
\parskip 0.5ex

\section{Introduction}

This Isabelle/HOL formalization defines recursive path orders (RPOs) for
higher-order terms without $\lambda$-abstraction and proves many useful
properties about them. The main order fully coincides with the standard RPO on
first-order terms also in the presence of currying, distinguishing it from
previous work. An optimized variant is formalized as well. It appears
promising as the basis of a higher-order superposition calculus.

We refer to the following conference paper for details:

\begin{quote}
Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand: \\
A Lambda-Free Higher-Order Recursive Path Order. \\
FoSSaCS 2017: 461-479 \\
\url{https://www.cs.vu.nl/~jbe248/lambda_free_rpo_conf.pdf}
\end{quote}

% generated text of all theories
\input{session}

% optional bibliography
%\bibliographystyle{abbrv}
%\bibliography{root}

%\bibliographystyle{abbrv}
%\bibliography{bib}

\end{document}
