The IJCAR 2008 Workshop on

Evaluation of Systems for Higher Order Logic

will be held 10-11th August 2008, as part of

The 4th International Joint Conference on Automated Reasoning
Sydney, Australia, 10th-15th August 2008

This workshop brings together practitioners and researchers who are involved in the development of reasoning systems based on higher-order logic. The workshop will stimulate and foster the build-up of an infrastructure that supports research, development, and deployment of higher-order reasoning systems. A particular focus is on means to evaluate higher-order reasoning systems. Advances in these aspects of reasoning in higher-order logic will make higher-order reasoning system easier to use in applications, e.g., hardware and software verification, knowledge based reasoning, and computer aided mathematics. The workshop's notion of higher-order includes, but is not limited to, ramified type theory, simple type theory, intuitionistic and constructive type theory, and logical frameworks. The workshop's notion of reasoning systems includes automated and semi-automated provers, model generators, as well as proof and model checkers. The workshop will have three parts:

We envision attendees that are interested in fostering the development and visibility of reasoning systems for higher-order logics, and the connection between research on the various flavors of higher-order logic. We are particularly interested in comparisons of the practical strengths of higher-order reasoning systems and in a discusssion on the development of a higher-order version of the TPTP. Due to the intricate nature of higher-order logic, we are also interested in a discussion on what practical strength means in the context of higher-order logic and how it can be measured.


The workshop will be a one-and-a-halfday workshop, organized as follows:

Program Committee
Peter Andrews
Andrea Asperti
Michael Beeson
Christoph Benzmüller
Chad Brown
Gilles Dowek
Viktor Kuncak
Dale Miller
Michael Norrish
Larry Paulson
Florian Rabe
Sandip Ray
Carsten Schürmann
Natarajan Shankar
Geoff Sutcliffe
Josef Urban

The workshop organizers are Christoph Benzmüller, Florian Rabe, Carsten Schürmann, and Geoff Sutcliffe, If you have any questions about the workshop, please email the organizers.

Journal Publication

A special issue of the Journal of Applied Logic, based around around the topic of the ESHOL workshop, is planned (the JAL has agreed), provided there are sufficiently many strong submissions. The special issue will target ESHOL participants, but will also also accept submissions from the broader community.


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, and a balanced program of high-quality contributions will be selected. Submissions must be in PDF, and must conform to the format produced by LaTeX with this template (this is what the PDF should look like). There is a 20 page limit. Long listings of problems or computer output should be relegated to a referenced WWW site.

Submission is via EasyChair (thanks to Andrei Voronkov). The selected contributions will be printed as workshop proceedings, and will also be published as CEUR Workshop Proceedings.

Important dates