Call for papers
General information
ITP is the premier international conference for researchers from all areas of interactive theorem proving and its applications. The inaugural meeting of ITP was held in July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC), the second meeting took place in Nijmegen, The Netherlands, in August 2011 and the third meeting was held in Princeton, New Jersey, in August 2012. ITP 2013 will take place in Rennes, France on 23-26 July 2013 with workshops preceding the main conference. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009.
The program committee welcomes submissions on all aspects of interactive theorem proving and its applications. Examples of typical topics include formal aspects of hardware or software (specification, verification, semantics, synthesis, refinement, compilation, etc.); formalization of significant bodies of mathematics; advances in theorem prover technology (automation, decision procedures, induction, combinations of systems and tools, etc.); other topics including those relating to user interfaces, education, comparisons of systems, and mechanizable logics; and concise and elegant worked examples ("Proof Pearls").
Submission details
All papers must be submitted electronically, via EasyChair.
Papers may be no longer than 16 pages and are to be submitted in PDF using the Springer LNCS format. Instructions and style files may be found by going to http://www.springer.com/computer/lncs/lncs+authors, and downloading the files llncs2e.zip and typeinst.zip. Submissions must describe original unpublished work not submitted for publication elsewhere, presented in a way that users of other systems can understand. The proceedings will be published as a volume in the Springer Lecture Notes in Computer Science series and will be available to participants at the conference.
In addition to regular submissions, described above, there will be a "rough diamonds" section. Rough diamond submissions are limited to six pages and may consist of an extended abstract. They will be refereed: they will be expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings, and will be presented as short talks.
Both regular and rough diamond submissions require an abstract of 70 to 150 words to be submitted electronically at the above address one week before the full submission. All submissions must be written in English. Submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. This material can be uploaded via easychair or made available online if a suitable URL is provided in the submitted paper. This material will not be accessed until February 15th (9 days after the paper submission deadline). Authors who have strong reasons (e.g. of commercial/legal nature) for violating this policy should contact the PC chairs in advance. At the time of abstract submission, proof assistants and other tools necessary for evaluating the submission should be indicated using the Keywords section of the web interface.
Authors of accepted papers are expected to present their papers at the conference, and will be required to sign copyright release forms. All submissions must be written in English.
Important Dates
| January 29th, 2013 | |
| February 6th, 2013 | |
| March 28th, 2013 | |
| April 22th, 2013 |