Call For Papers

The International Conference on Interactive Theorem Proving (ITP 2026) will take place on 26-29 July, 2026 in Lisbon, Portugal. It will be part of FLoC 2026. ITP 2026 is part of the ITP conference series whose history goes back to 1988.

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 17th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988.

Paper Submission

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:

• formalizations of computational models
• improvements in interactive theorem prover technology
• formalizations of mathematics
• integration with automated provers and other symbolic tools
• verification of security algorithms
• industrial applications of interactive theorem provers
• formal specification and verification of hardware and software
• user interfaces for interactive theorem provers
• use of theorem provers in education
• concise and elegant worked examples of formalizations (proof pearls)

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.

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:

• be no more than 16 pages in length excluding bibliographic references
• not include an appendix, and
• be in LIPIcs format.

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

• be no more than 6 pages in length excluding bibliographic references and may consist of an extended abstract,/li>
• have the phrase "Short paper" as a subtitle,
• not include an appendix, and
• be in LIPIcs format.

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. All submissions are expected to be accompanied by anonymised supplementary material containing verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used.

Publication Details

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.