The 4th International Joint Conference on
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:
The systems described in the second part will be demonstrated. Moreover, a first competition "happening" for automated theorem provers for simple type theory is planned. This competition will be similar to the CASC competition for first-order reasoning systems. It will exploit and test the TPTP problem representation language for simple type theory, which was recently developed by the organizers.
The workshop will be a one-and-a-halfday workshop, organized as follows:
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.
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.