Paper Submission and Presentation

Papers should be submitted using the TPHOLs 2008 submission system hosted by Easy Chair. 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.

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.

Full research papers will be published in a volume of the Springer series Lecture Notes in Computer Science (LNCS). These papers should be no more than 16 pages and 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 LNCS for Authors page. Please use the latest version of the LNCS style file. The initial verison of the paper should be submitted as a PDF file.

If the paper is accepted, you should submit the final version of the paper as an archive (*.zip or *.tgz) containing a PDF file along with all source files needed to compile the paper. This includes all text files, all figure files and all macro and style files except those included in a standard teTeX distribution. Additionally, we need a signed LNCS Consent to Publish before your paper can be included in the proceedings. Please fax it to +1(514)848-2802

Camera-ready copy due: 15 May 2008

Emerging Trends

The purpose of this category 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 emerging trends paper track will include short talks and poster sessions. Those submissions accepted will also be published in a technical report, which will be available at the conference. Emerging trends 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. Papers must be no more than the equivalent of 16 pages of an LNCS volume in length (much less is fine). The initial verison of the paper should be submitted as a PDF file.

Submissions should be sent electronically directly to the organizers using the email address "tphols08@ece.concordia.ca". This email address can also be used for any inquiries concerning the conference.

If the paper is accepted, you should submit the final version of the paper as a PDF file. Please do not use any page numbers, since they will be added after the compilation of the proceedings.

Camera-ready copy due: 25 Jul 2008

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. 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.

Presentations

Presenters of Category A papers (Full Research Papers) have 30 minutes for their talks (including questions). The time limit for Category B papers (Emerging Trends) is 10 minutes. Directly after the talks, questions can be asked during a poster session. Authors should prepare a poster (max. size: A0, 841mm × 1189mm, 33.11 inch X 46.81 inch).

For your TPHOLs 2008 talk we will provide a presentation system which features both Microsoft Powerpoint (Version: Office 2003 or 2007) and Adobe Acrobat Reader (Version 8). Please check that your presentation works with either program version correctly. Please email your presentation before the conference no later than Monday, 11 August 2008 to the conference organisers and mark in the Subject line of your email the submission number as well as the title of your presentation. We will then install your presentation for you. You can still update on-site your presentation stored on a USB stick, but this is intended for emergency cases only.