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

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

\noindent\textbf{#1}}
\newcommand{\tmop}[1]{\ensuremath{\operatorname{#1}}}
\newcommand{\tmstrong}[1]{\textbf{#1}}
\newcommand{\tmtextbf}[1]{{\bfseries{#1}}}
\newcommand{\tmtextrm}[1]{{\rmfamily{#1}}}
\newcommand{\tmtextsf}[1]{{\sffamily{#1}}}
\definecolor{grey}{rgb}{0.75,0.75,0.75}
\definecolor{orange}{rgb}{1.0,0.5,0.5}
\definecolor{brown}{rgb}{0.5,0.25,0.0}
\definecolor{pink}{rgb}{1.0,0.5,0.5}
%%%%%%%%%% 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}

{\color{red} \begin{center}
  The workshop is open for all registered LPAR attendees
\end{center}}

\begin{center}
  (\href{http://arxiv.org/abs/cs/0601042}{Proceedings in arxiv.org})
\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 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 demonstrations}}.

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*{Timetable}

\begin{tabular}{ll}
  09:00-10:00 & Invited Talk \\
  & \tmtextbf{\tmtextrm{Joe Hurd (Oxford): }}\\
  &  First Order Proof for Higher Order Logic Theorem Provers
  (\href{final-versions/1-Hurd.pdf}{pdf})\\
  10:00-10:30 & Coffee Break\\
  10:30-12:30 & Paper Session I (30min each)\\
  & \tmtextbf{\tmtextrm{Michael Beeson:}}\\
  &  Implicit Typing in Lambda Logic
  (\href{final-versions/2-Beeson.pdf}{pdf})\\
  & \tmtextbf{\tmtextrm{Christoph Benzm\"uller:} }\\
  &  LEO -- A Resolution based Higher Order Theorem Prover \
  (\href{final-versions/3-Benzmueller.pdf}{pdf})\\
  & \tmtextbf{\tmtextrm{Christoph Benzm\"uller, Volker Sorge, Mateja Jamnik
  and Manfred Kerber:}} \\
  &  Combining Proofs of Higher-Order and First-Order Automated Theorem
  Provers \ (\href{final-versions/4-BenzmuellerEtAl.pdf}{pdf})\\
  12:30-13:30 & Lunch Break\\
  13:30-14:30 & Invited Talk \\
  & \tmtextbf{\tmtextrm{Chad Brown (Saarbr\"ucken):}}\\
  &  \ Benchmarks for Higher-Order Automated Reasoning
  (\href{final-versions/5-Brown.pdf}{pdf})\\
  14:30-15:30 & Paper Session II (30min each, chair: TBA)\\
  & \tmtextbf{\tmtextrm{Jutta Eusterbrock:} \ }\\
  &  Co-Synthesis of New Complex Selection Algorithms and their Human
  Comprehensible XML Documentation
  (\href{final-versions/6-Eusterbrock.pdf}{pdf})\\
  & \tmtextbf{\tmtextrm{Alwen Tiu, Gopalan Nadathur and Dale Miller:} }\\
  &  Mixing Finite Success and Finite Failure in an Automated Prover
  (\href{final-versions/7-TiuEtAl.pdf}{pdf})\\
  15:30-16:00 & Coffee Break\\
  16:00-17:00 & System Demonstrations (15min each)\\
  & \tmtextbf{\tmtextrm{Michael Beeson:} }\\
  &  Otter-$\lambda$ (\href{final-versions/8-Beeson-System.pdf}{pdf})\\
  & \tmtextbf{\tmtextrm{Chad Brown}:} \\
  &  TPS (\href{final-versions/9-Brown-System.pdf}{pdf})\\
  & \tmtextbf{\tmtextrm{Joe Hurd:} }\\
  &  Metis (\href{final-versions/10-Hurd-System.pdf}{pdf})\\
  & \tmtextbf{\tmtextrm{Christoph Benzm\"uller:} }\\
  &  LEO\\
  17:00-18:00 & Discussion: Higher-Order TPTP -- Feasible or Not?\\
  & Chair and Panelists: TBA\\
  & 
\end{tabular}

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

\section*{Organization}

\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}

The original CFP can be found \href{cfp.html}{here}.

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

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

\end{document}