The LPAR 2005 Workshop on
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.
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 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 ESCAR and ESFOR workshops held at CADE 2005 and IJCAR 2004.
The workshop will be a 1 day workshop organized as follows:
| Peter Andrews | Carnegie Mellon University, USA |
| Michael Beeson | San Jose State University, USA |
| Chad Brown | Saarland University, Germany |
| Gilles Dowek | É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 |
| Christoph Benzmüller | Saarland University, Germany |
| John Harrison | Intel Corporation, USA |
| Carsten Schürmann | Yale University, USA |
If you have any questions about the workshop, please email the organizers.
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 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 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:
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 link to the ESHOL'05 submission website.
The 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.
This page is also available as pdf.