| [Guide for Authors] [Typesetting Requirements] |
Formal 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. Work in progress papers will be published in a technical report, but should also be prepared in the LNCS style so that the two volumes have a consistent look and feel. Complete instructions on how to typeset your paper in the style of the series can be obtained from the typesetting instructions page.
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 18 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.
| Deadline for research paper submissions: | February, 28th 1999 |
| Research paper acceptance notification: | April, 15th 1999 |
| Camera-ready copy for research papers due: | May, 12th 1999 |
| Deadline for progress paper submissions: | May, 19th 1999 |
| Progress paper acceptance notification: | June, 30th 1999 |
| Camera-ready copy for progress papers due: | July, 25th 1999 |
| Conference: | September, 14-17 1999 |
One author of each formal research paper must complete and return a form transferring the copyright for the paper to Springer-Verlag. The form is available for download in either PDF or HTML formats. You will need the following information to complete the form:
Once you have completed the form, please fax it to Laurent Théry +33 4 92 38 76 33.
The TPHOLs community is drawn from users of a variety of tools for reasoning in higher order logic. You should strive to ensure that wherever possible your paper is accessible to the broader TPHOLs community, not just other users of the same theorem proving 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
| ¬(even (j·k3 + k + 1)) | or | ¬(even (j·k3 + k + 1)) |
| for ordinary mathematics | to emphasise machine checking |
in preference to
the same expression in the concrete syntax of, for example, the HOL system.
Of course, you may need to use concrete syntax in your paper - for example, if the syntax itself is under discussion - but please explain any aspects that are not obvious.
| [Guide for Authors] [Typesetting Requirements] |