\documentclass{llncs}
\usepackage{epsfig}

\begin{document}
\title{\huge {\Large LPAR-05 Workshop:} \\
Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL)}
\institute{}

\author{\large Christoph Benzm\"uller, John Harrison, and Carsten Sch\"urmann (eds.)}

\maketitle

\vspace*{2cm}

\begin{center}
\epsfig{file=../bild.eps,width=6cm}
\end{center}

\vspace*{2cm}

\begin{center}
\Large Wexford Hotel, Montego Bay, Jamaica\\ December 2nd, 2005
\end{center}


\newpage
\phantom{bla}

\newpage


\section*{The ESHOL-05 Workshop} 
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 includes system demonstrations.

ESHOL is the successor of the ESCAR and ESFOR workshops held at CADE 2005 and IJCAR 2004. \\[1cm]

November, 2005
\begin{flushright}
\begin{tabular}{l@{\hspace{.5cm}}l}
Christoph Benzm\"uller & Saarland University, Germany\\
John Harrison & Intel Corporation, USA\\
Carsten Sch\"urmann & IT University of Copenhagen, Denmark
\end{tabular}
\end{flushright}

\vspace*{2cm}

\textbf{Programme Committee}\\

\noindent
\begin{tabular}{l@{\hspace{.5cm}}l}
Peter Andrews  &	Carnegie Mellon University, USA \\
Michael Beeson & 	San Jose State University, USA \\
Chad Brown &	Saarland University, Germany \\
Gilles Dowek & 	\'{E}cole Polytechnique, France \\ 
Christoph Kreitz &	Potsdam University, Germany \\
Larry Paulson &	Cambridge University, UK \\
Frank Pfenning & 	Carnegie Mellon University, USA \\
Geoff Sutcliffe &	University of Miami, USA \\
Volker Sorge &	University of Birmingham, UK \\
Freek Wiedijk &	Nijmegen University, Netherlands \\
\end{tabular}

\pagebreak

\section*{Schedule (December 2nd, 2005)}
\vspace*{1cm}

\begin{tabular}{l@{\hspace{.5cm}}l}
09:00-10:00  & 	Invited Talk \\ \\
             & \begin{minipage}{10cm}
               \textbf{Joe Hurd (Oxford):} First Order Proof for Higher Order Logic Theorem Provers  \\
               \end{minipage} \\
10:00-10:30 &	Coffee Break \\ \\
10:30-12:30 &	Paper Session I  \\ \\
	    & \begin{minipage}{10cm} \textbf{Michael Beeson:} Implicit Typing in Lambda Logic \\ \end{minipage} \\
	    & \begin{minipage}{10cm} \textbf{Christoph Benzm{\"u}ller:}	LEO -- A Resolution based Higher Order Theorem Prover\\ \end{minipage} \\
	& \begin{minipage}{10cm} \textbf{Christoph Benzm\"uller, Volker Sorge, Mateja Jamnik and Manfred Kerber:} 
	Combining Proofs of Higher-Order and First-Order Automated Theorem Provers\\ \end{minipage} \\
12:30-13:30 &	Lunch Break \\ \\
13:30-14:30 &	Invited Talk \\ \\
	& \begin{minipage}{10cm} \textbf{Chad Brown (Saarbr\"ucken):}
	Benchmarks for Higher-Order Automated Reasoning \\ \end{minipage} \\
14:30-15:30 &	Paper Session II  \\ \\
	& \begin{minipage}{10cm} \textbf{Jutta Eusterbrock:} 
	Co-Synthesis of New Complex Selection Algorithms and their Human Comprehensible XML Documentation \\ \end{minipage} \\
	& \begin{minipage}{10cm} \textbf{Alwen Tiu, Gopalan Nadathur and Dale Miller:}
	Mixing Finite Success and Finite Failure in an Automated Prover \\ \end{minipage} \\
15:30-16:00 &	Coffee Break \\ \\
16:00-17:00 &	System Demonstrations \\ \\
	& \begin{minipage}{10cm} \textbf{Michael Beeson:}
	Otter-$\lambda$  \end{minipage} \\ \\
	& \begin{minipage}{10cm} \textbf{Chad Brown:}
	TPS \end{minipage} \\  \\
	& \begin{minipage}{10cm} \textbf{Joe Hurd:}
	Metis \end{minipage} \\ \\
	& \begin{minipage}{10cm} \textbf{Christoph Benzm\"uller:}
	LEO \end{minipage} \\ \\
17:00-18:00 &	Discussion: Higher-Order TPTP -- Feasible or Not? \\
	& Chair and Panelists: TBA
\end{tabular}
	
\pagebreak

\section*{Table of Contents}

\newcommand{\tocTitle}[2]{\contentsline{title}{#1}{#2}}
\newcommand{\tocAuthors}[1]{{\raggedright \leftskip 15pt \rightskip 2.55em\itshape #1\endgraf}}
\newcommand{\tocSection}[2]{\contentsline{chapter}{#1. \textmd{#2}}{0}}


% yet unsorted papers
 \tocTitle{First Order Proof for Higher Order Logic Theorem Provers (invited talk, abstract)}{1}
    \tocAuthors{Joe Hurd}

  \tocTitle{Implicit Typing in Lambda Logic}{5}
    \tocAuthors{Michael Beeson}

 \tocTitle{System Description: {LEO} -- A Resolution based Higher Order Theorem Prover}{25}
    \tocAuthors{Christoph Benzm\"uller}

  \tocTitle{Combining Proofs of Higher-Order and First-Order Automated Theorem Provers}{45}
    \tocAuthors{Christoph Benzm\"uller, Volker Sorge, Mateja Jamnik, Manfred Kerber}

  \tocTitle{Benchmarks for Higher-Order Automated Reasoning (invited talk, abstract)}{59}
    \tocAuthors{Chad Brown}

  \tocTitle{Co-Synthesis of New Complex Selection Algorithms and their Human Comprehensible XML Documentation}{61}
    \tocAuthors{Jutta Eusterbrock}
 

  \tocTitle{Mixing Finite Success and Finite Failure in an Automated Prover}{79}
    \tocAuthors{Alwen Tiu, Gopalan Nadathur, Dale Miller}

  \tocTitle{Otter-$\lambda$ (system demonstration, abstract)}{99}
    \tocAuthors{Michael Beeson}

  \tocTitle{TPS (system demonstration, abstract)}{101}
    \tocAuthors{Chad Brown}

  \tocTitle{Metis (system demonstration, abstract)}{103}
    \tocAuthors{Joe Hurd}

\newpage
\phantom{bla}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: