\documentclass{letter}
\usepackage{amsmath,epsfig,hyperref}

%%%%%%%%%% Start TeXmacs macros
\newcommand{\paragraph}[1]{\smallskip

\noindent\textbf{#1}}
\newcommand{\tmop}[1]{\ensuremath{\operatorname{#1}}}
\newcommand{\tmstrong}[1]{\textbf{#1}}
\newcommand{\tmtextsf}[1]{{\sffamily{#1}}}
\newenvironment{tmparsep}[1]{\begingroup\setlength{\parskip}{#1}}{\endgroup}
%%%%%%%%%% End TeXmacs macros

\begin{document}

\tmtextsf{The $\href{\tmop{http} : / / \tmop{www} . \tmop{cs} . \tmop{miami} .
\tmop{edu} / \tmop{geoff} / \tmop{Conferences} / \tmop{LPAR} - 12
/}{\tmop{LPAR} 2005}$ Workshop on

{\noindent}\begin{tabular}{l}
  \hline
  \quad
\end{tabular}

\begin{center}
  \epsfig{file=header.gif}
\end{center}

{\noindent}\begin{tabular}{l}
  \hline
  \quad
\end{tabular}

This workshop brings together practioners and researchers who are involved in
the everyday aspects of logical systems based on higher-order logic. \ We hope
to create a friendly and highly interactive setting for discussions around the
following four topics. Implementation and development of proof assistants
based on any notion of impredicativity, automated theorem proving tools for
higher-order logic reasoning systems, logical framework technology for the
representation of proofs in higher-order logic, formal digital libraries for
storing, maintaining and querying databases of proofs. \ We solicit paper
submissions within or related to the following two areas.

\paragraph{Systems}

\begin{tmparsep}{0em}
  \begin{itemize}
    \item Tactic-based proof assistants. Heuristics.
    
    \item Automated theorem proving. \ Proof search. Resolution. Equational
    theories.
    
    \item Implementation. Higher-order unification. Term-indexing.
    
    \item Logical frameworks. Meta-languages for logical formulas and proofs.
    
    \item Formal digital libraries of mathematical proof. \ Database
    technology. Query languages.
    
    \item Integration of Reasoning Systems. 
  \end{itemize}
\end{tmparsep}

\paragraph{Applications}

\begin{tmparsep}{0em}
  \begin{itemize}
    \item Comparative analysis of higher-order reasoning techniques.
    
    \item Experience reports. \ Integration and cooperations with their
    logics, constraint solvers, model generators, and model checkers.
    
    \item Special purpose reasoning techniques for practical applications.
    
    \item User interfaces.
    
    \item Practical results of proof representation and compression.
    
    \item Logic morphisms.
    
    \item Digital libraries. Benchmark problems. Challenge problems. 
  \end{itemize}
\end{tmparsep}

We envision attendees that are interested in fostering the development and
visibility of reasoning systems for higher-order logics. We are particularly
interested in a discusssion on the development of a higher-order version of
the TPTP and in comparisons of the practical strengths of automated
higher-order reasoning systems.

Additionally, the workshop will include {\tmstrong{system and application
demonstrations}}. Demonstrations of systems and applications described in
paper presentations, and demonstrations of systems and applications without an
accompanying paper, are both encouraged.

ESHOL is the successor of the \href{http://www.cs.miami.edu/\~{
}geoff/Conferences/ESCAR/}{ESCAR} and \href{http://www.cs.miami.edu/\~{
}geoff/Conferences/ESFOR/}{ESFOR} workshops held at CADE 2005 and IJCAR 2004.

{\noindent}\begin{tabular}{l}
  \hline
  \quad
\end{tabular}

\section*{Organization}

\paragraph{Structure of the Workshop}

The workshop will be a 1 day workshop organized as follows:

\begin{tmparsep}{0em}
  \begin{itemize}
    \item Presentation sessions, system demonstrations
    
    \item Invited talk
    
    \item Panel Discussion (or similarly organized event): How can we built-up
    a higher-order TPTP to foster the improvement of automated higher-order
    reasoning systems and their comparison with first-order theorem provers? 
  \end{itemize}
\end{tmparsep}

\paragraph{Programme Committee}

\begin{tabular}{ll}
  \href{http://gtps.math.cmu.edu/andrews.html}{Peter Andrews} & Carnegie
  Mellon University, USA\\
  \href{http://www.mathcs.sjsu.edu/faculty/beeson/}{Michael Beeson} & San Jose
  State University, USA\\
  \href{http://gtps.math.cmu.edu/cebrown/index.html}{Chad Brown} & Saarland
  University, Germany\\
  \href{http://www.lix.polytechnique.fr/\~{ }dowek/}{Gilles Dowek} & \'Ecole
  Polytechnique, France\\
  \href{http://www.cs.uni-potsdam.de/ti/kreitz/}{Christoph Kreitz} & Potsdam
  University, Germany\\
  \href{http://www.cl.cam.ac.uk/users/lcp/}{Larry Paulson} & Cambridge
  University, UK\\
  \href{http://www-2.cs.cmu.edu/\~{ }fp/}{Frank Pfenning} & Carnegie Mellon
  University, USA\\
  \href{http://www.cs.miami.edu/\~{ }geoff/}{Geoff Sutcliffe} & University of
  Miami, USA \\
  \href{http://www.cs.bham.ac.uk/\~{ }vxs/index.html}{Volker Sorge} &
  University of Birmingham, UK \\
  \href{http://www.cs.ru.nl/\~{ }freek/}{Freek Wiedijk} & Nijmegen University,
  Netherlands
\end{tabular}

\paragraph{Organizers and PC Chairs}

\begin{tabular}{ll}
  \href{http://www.ags.uni-sb.de/\~{ }chris}{Christoph Benzm\"uller} &
  Saarland University, Germany\\
  \href{http://www.cl.cam.ac.uk/users/jrh/}{John Harrison} & Intel
  Corporation, USA\\
  \href{http://cs-www.cs.yale.edu/homes/carsten/}{Carsten Sch\"urmann}  & Yale
  University, USA 
\end{tabular}

If you have any questions about the workshop, please
\href{mailto:eshol05@ags.uni-sb.de}{email the organizers}.

{\noindent}\begin{tabular}{l}
  \hline
  \quad
\end{tabular}

\section*{Submission}

Submission of papers for presentation at the workshop, and proposals for
system and application demonstrations at the workshop, are now invited.
Submissions will be reviewed (using \href{review-form}{this review form}), and
a balanced program of high-quality contributions will be selected. Submissions
can be in PDF or Postscript, and must conform to the format produced by LaTeX
with \href{http://www.cs.miami.edu/\~{
}geoff/Conferences/ESCAR/Workshop.tex}{this template}. There is a 20 page
limit. Long listings of problems or computer output should be relegated to a
referenced WWW site.

Proposals for system and application demonstrations must include:

\begin{tmparsep}{0em}
  \begin{itemize}
    \item System name, developers names and contact details.
    
    \item A system description, or associated paper submission.
    
    \item Screen shots or information for online access.
    
    \item Details of hardware and software that will have to be provided by
    the organizers if the demonstration is approved.
  \end{itemize}
\end{tmparsep}

Those who submit proposals are encouraged to provide evidence that the system
or application is empirically successful.

Submission is via EasyChair (thanks to Andrei Voronkov). Here is the
\href{http://www.easychair.org/ESHOL-05/submit/}{link to the ESHOL'05
submission website}.

\paragraph{Important Dates}

\begin{tmparsep}{0em}
  \begin{itemize}
    \item Submission deadline - September 28th
    
    \item Notification of acceptance - November 1st
    
    \item Camera ready versions due - November 10th
    
    \item Workshop - December 2nd
  \end{itemize}
\end{tmparsep}

{\noindent}\begin{tabular}{l}
  \hline
  \quad
\end{tabular}

\section*{Journal Publication}

The
\href{http://www.elsevier.com/wps/find/journaldescription.cws\_home/672712/description\#description}{Journal
of Applied Logic} has agreed to a special issue on empirically successful
higher-order automated reasoning. Authors of ESHOL papers will be able to
submit extended versions of their workshop papers for this special issue. All
papers submitted for the special issue will be reviewed according to the
journal's standards.

{\noindent}\begin{tabular}{l}
  \hline
  \quad
\end{tabular}

This page is also available as \href{cfp.pdf}{pdf}.}

\end{document}