ITP '25: Call for Papers

The 16th International Conference on Interactive Theorem Proving (ITP '25) is part of FroCoS/ITP/TABLEAUX '25 and will be held in Reykjavik, Iceland, from September 29 to October 2, 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

Important Dates

• Abstract submission deadline: March 12, 2025
• Paper submission deadline: March 19, 2025
• Author notification: May 23, 2025
• Camera-ready copy due: June 27, 2025

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:

• 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)

Paper Categories and Submission

We welcome regular papers and short papers.

Submission Process

Submission for both categories is lightweight double-blind. This means that:

1. Author names and institutions must be omitted using the anonymous option of the document class.
2. References to authors’ own related work should be in the third person.
3. The identity of authors will be revealed to reviewers once they have submitted a first draft of their review.

Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing it more difficult. Important background references should not be omitted or anonymized. Authors are free to disseminate their ideas or draft versions of their papers as usual.

Regular Papers

• Must be no more than 16 pages in length excluding bibliographic references.
• Must not include an appendix.
• Must 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.
• Must be no more than 6 pages in length excluding bibliographic references and may consist of an extended abstract.
• Must have the phrase "Short paper" as a subtitle.
• Must not include an appendix.
• Must be in LIPIcs format.

Formatting and Submission Platform

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.

Supplementary Material

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.

• Anonymous supplementary material is made available to the reviewers before they submit their first-draft reviews.
• 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, physical participation is strongly encouraged.
• 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 Co-chairs

• Yannick Forster, Inria Paris
• Chantal Keller, LMF, Université Paris-Saclay

Accepted Papers

• A Certified Proof Checker for Deep Neural Network Verification in Imandra
• A Formal Analysis of Algorithms for Matroids and Greedoids
• A Formal Proof of Complexity Bounds on Diophantine Equations
• A Formalization of Divided Powers in Lean
• A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching
• A Natural Language Formalization of Perfectoid Rings in Naproche
• A Verified Cost Model for Call-by-Push-Value
• Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness a la Fitting
• Algebra is half the battle: Verifying presentations for graded unipotent Chevalley groups
• An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems
• Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL
• Automatically Generalizing Proofs and Statements
• Barendregt's Theory of the Lambda-Calculus, Refreshed and Formalized
• Canonical for Automated Theorem Proving in Lean
• Certified Implementability of Global Multiparty Protocols
• Finiteness of symbolic derivatives in Lean
• Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic
• Formalising Inductive and Coinductive Containers
• Formalising New Mathematics in Isabelle: Diagonal Ramsey
• Formalising Subject Reduction and Progress for Multiparty Session Processes
• Formalizing colimits in Cat
• Formalizing concentration inequalities in Rocq: infrastructure and automation
• Formalizing Splitting in Isabelle/HOL
• Formalizing the Hidden Number Problem in Isabelle/HOL
• Formally verifying a vertical cell decomposition algorithm
• GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
• Hammering without ATPs (short paper)
• Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL
• LeanLTL: A unifying framework for linear temporal logics in Lean (Short Paper)
• Mechanising Böhm Trees and λη-Completeness
• Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
• Nondeterministic Asynchronous Dataflow in Isabelle/HOL
• Program Optimisations via Hylomorphisms for Extraction of Executable Code
• Scott’s Representation Theorem and the Univalent Karoubi Envelope
• Towards Automating Permutation Proofs in Coq: A Reflexive Approach with Iterative Deepening Search (Short Paper)
• Verification of the CVM algorithm with a Functional Probabilistic Invariant
• Verified Elimination of Secret Control-Flow
• Verifying an Efficient Algorithm for Computing Bernoulli Numbers
• Verifying Datalog Reasoning with Lean