16th International Conference on Interactive Theorem Proving

ITP '25

part of FroCoS/ITP/TABLEAUX '25

Reykjavik, Iceland, 27 September-3 October 2025

Background

The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics. This will be the 16th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988.

Invited speakers

tba

Call for papers

Important dates

Topics

ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include, but are not limited to, the following:

Paper categories and submission

We welcome regular papers and short papers. Submission for both is lightweight double-blind. This means that (1) author names and institutions must be omitted using the the anonymous option of the document class, (2) references to authors’ own related work should be in the third person, and (3) the identity of authors will be reveiled to reviewers once they have submitted a first draft of their review.

The purpose of this process is to help the PC and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing it more difficult. In particular, important background references should not be omitted or anonymized. In addition, authors are free to disseminate their ideas or draft versions of their papers as usual. For example, authors may post drafts of their papers on the web or give talks on their research ideas.

Regular papers must:

Short papers can be used to describe interesting work that is still ongoing and not fully mature. Accepted short papers will be published in the main proceedings and will be presented as short talks. Short papers must

Both categories of papers must be prepared in LaTeX using the lipics-v2021 style (v2021.1.3) and must be submitted electronically as pdf files through HotCRP (link tba).

All submissions are expected to be accompanied by supplementary material containing verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used.

Two forms of supplementary material may be submitted: (1) Anonymous supplementary material is made available to the reviewers before they submit their first-draft reviews. (2) Non-anonymous supplementary material is made available to the reviewers after they have submitted their first-draft reviews and have learned the identity of the authors. We strongly encourage anonymous supplementary material whenever possible.

Publication

The conference proceedings will be published in Dagstuhl Publishing's Leibniz International Proceedings in Informatics (LIPIcs) series in Gold Open Access under the CC-BY-4.0 license.

Registration and Participation

Remote attendance of the conference will be possible for a low or no fee. For all accepted papers, at least one author must pay a full registration fee. For presenters we strongly encourage physical participation since coming to the conference benefits the dissemination of the paper and the overall quality of the conference. Remote talks are only possible if agreed with the organizers by the registration deadline, but still one author must pay the full registration fee.

Programme committee cochairs

Programme committee

Organizers, sponsors and local information

See the shared pages of the colocated conferences.

Last update 14 January 2025