The 14th International Conference on Theorem Proving in Higher Order Logics
3-6 September 2001, Edinburgh, Scotland

[Home Page][Conference History][Call for Papers][Guide for Authors][Programme] 
[Related Events][How to Get There][Weather and Tourism][Registration][Accommodation] 
[Sponsors][Student Bursaries][Proceedings][Photos][Business Meeting][TPHOLs 2002]

Guide for Authors

Full Research Papers

Submitted papers will be judged on the basis of relevance, significance, correctness, originality, and clarity. They should include a clear identification of what has been accomplished and why it is significant. Submissions must include an abstract and a discussion of related work. They must describe work that has not previously been published in a major forum. The authors should indicate if a closely related paper is also being considered for another conference or journal.

Research papers will be published in a volume of the Springer-Verlag series Lecture Notes in Computer Science (LNCS). These papers must be prepared in the style of that series. Complete instructions on how to typeset your paper in the style of the series can be obtained from the typesetting instructions page. Please use the latest version of the LNCS style file.

In general, the length of a paper should be commensurate with the contribution it makes. The final versions of all papers, however, must be kept to 16 pages or less when formatted in the LNCS style. It may be advisable to begin to prepare your document in something approximating the LNCS style from an early stage so that you have an accurate knowledge of its length when presented in this format.

Short Work-in-Progress Papers

The purpose of the work-in-progress paper track is to provide an informal forum for the presentation of recent work, preliminary results, and even highly-speculative ideas. Following the tradition of past TPHOLs, the work-in-progress paper track will include short talks (about 5 minutes) and poster sessions. Those submissions accepted will also be published in a technical report, which will be available at the conference. Work-in-progress papers will not be formally refereed, but their content and relevance will be reviewed.

Please use the LNCS style in preparing your camera ready copy. See the typesetting instructions page for details. Be careful about staying within the page boundaries specified by this style and don't change the style formatting (font size, line spacing etc.). Your camera ready copy will be reduced in size slightly to fit in an A5 page, and it's important that it remains legible. Use

\documentclass[runningheads]{llncs}
\pagestyle{headings}
\setcounter{page}{1}

at the start of your .tex document and make sure that \authorrunning and \titlerunning are set appropriately. Use initials and lastname of each author for the \authorrunning format. Don't use \toctitle or \tocauthor.

Papers must be no more than the equivalent of 16 pages of an LNCS volume in length (much less is fine), and camera ready copy must be no more than one page longer than the initial submission. These limits are essential for us to be able to print all the category B submissions.

Important Dates

Submitting Papers

Papers should be submitted using the Web forms on the electronic submission page. Please do not submit papers by e-mail to any of the conference organisers or the conference e-mail address unless you have been advised to do so by the Programme Chair.

Initial Submissions

Camera-Ready Copy

• all text files,
• all figure files,
• all macro and style files except those included in a standard TeTeX distribution.

Writing for the TPHOLs community

The TPHOLs community is drawn from users of a variety of theorem proving tools. You should strive to ensure that wherever possible your paper is accessible to the broader TPHOLs community, not just other users of the same tool that you use. At least one reviewer for each tool-based research paper submitted to TPHOLs will be deliberately drawn from the users of a different theorem proving tool. Reviewers will be asked to judge, among other things, the accessibility of the paper to the wider TPHOLs audience.

One barrier to effective communication, both within the TPHOLs community and between the TPHOLs community and other communities, is the variety of concrete syntaxes used by different theorem proving tools for mathematical notation that is unavailable in standard character sets. To avoid this problem we ask that where possible you use common mathematical notations in your paper rather than the concrete syntax of any particular theorem prover. To emphasise that mathematics has been machine checked you may like to depart from the LNCS style and use a Teletype or Sans-Serif font for the text of your expressions rather than the mandated Roman and Italic fonts. For example, you should write something like

in preference to

the same expression in the concrete syntax of, for example, the HOL system.

Authors who decide it is important to use a particular concrete syntax should do whatever is possible to make their papers intelligible to the mathematically literate reader unfamiliar with that syntax.