16th International Conference on Interactive Theorem Proving
ITP '25
Reykjavik, Iceland, 27 September-3 October 2025
News
Accepted papers are out, see below!
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
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, 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)
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:
- 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,
- 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 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
- Mohammad Abdulaziz, King's College London
- Reynald Affeldt, AIST
- Jeremy Avigad, Carnegie Mellon University
- Anne Baanen, Vrije Universiteit Amsterdam, Lean FRO LLC
- Małgorzata Biernacka, University of Wroclaw
- Mario Carneiro, Chalmers University of Technology
- Évelyne Contejean, CNRS
- María Inés de Frutos Fernández, University of Bonn
- Tom de Jong, University of Nottingham
- Thaynara Arielly de Lima, Universidade Federal de Goiás
- Manuel Eberl, University of Innsbruck
- Chelsea Edmonds, University of Sheffield
- Andres Erbsen, Google
- Thiago Felicissimo, Inria Rennes
- Amy Felty, University of Ottawa
- Asta Halkjær From, University of Copenhagen
- Aymeric Fromherz, Inria Paris
- Ruben Gamboa, University of Wyoming
- Hrutvik Kanabar, Arm
- Dominik Kirst, Inria
- Angeliki Koutsoukou-Argyraki, Royal Holloway, University of London and University of Cambridge
- Vincent Laporte, Inria Nancy
- Meven Lennon-Bertrand, University of Cambridge
- Robert Lewis, Brown University
- Heather Macbeth, Fordham University, NYC
- Cody Roux, AWS
- Yong Kiam Tan, Institute for Infocomm Research, A*STAR, Singapore
- Andrew Tolmach, Portland State University
- Sophie Tourret, Inria Nancy
- Dmitriy Traytel, University of Copenhagen
- Niccolò Veltri, Tallinn University of Technology
- Bohua Zhan, Huawei Technologies Co., Ltd.
Accepted papers
- A Certified Proof Checker for Deep Neural Network Verification in Imandra
Remi Desmartin, Omri Isac, Ekaterina Komendantskaya, Kathrin Stark, Grant Passmore, Guy Katz
- A Formal Analysis of Algorithms for Matroids and Greedoids
Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa, Mohammad Abdulaziz
- A Formal Proof of Complexity Bounds on Diophantine Equations
Jonas Bayer, Marco David
- A Formalization of Divided Powers in Lean
Antoine Chambert-Loir, María Inés de Frutos-Fernández
- A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching
Joshua M. Cohen
- A Natural Language Formalization of Perfectoid Rings in Naproche
Peter Koepke
- A Verified Cost Model for Call-by-Push-Value
Zhuo Chen, Johannes Åman Pohjola, Christine Rizkallah
- Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness a la Fitting
Asta Halkjær From, Anders Schlichtkrull
- Algebra is half the battle: Verifying presentations for graded unipotent Chevalley groups
Eric Wang, Arohee Bhoja, Cayden Codel, Noah G. Singer
- An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems
Dohan Kim
- Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL
Jan van Brügge, Andrei Popescu, Dmitriy Traytel
- Automatically Generalizing Proofs and Statements
Anshula Gandhi, Anand Rao Tadipatri, Timothy Gowers
- Barendregt's Theory of the Lambda-Calculus, Refreshed and Formalized
Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs
- Canonical for Automated Theorem Proving in Lean
Chase Norman, Jeremy Avigad
- Certified Implementability of Global Multiparty Protocols
Elaine Li, Thomas Wies
- Finiteness of symbolic derivatives in Lean
Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner
- Fixpoints in Higher-Order Separation Logic
Robbert Krebbers, Luko van der Maas, Enrico Tassi
- Formalising Inductive and Coinductive Containers
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
- Formalising New Mathematics in Isabelle: Diagonal Ramsey
Lawrence Paulson
- Formalising Subject Reduction and Progress for Multiparty Session Processes
Burak Ekici, Tadayoshi Kamegai, Nobuko Yoshida
- Formalizing colimits in Cat
Mario Carneiro, Emily Riehl
- Formalizing concentration inequalities in Rocq: infrastructure and automation
Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa
- Formalizing Splitting in Isabelle/HOL
Ghilain Bergeron, Florent Krasnopol, Sophie Tourret
- Formalizing the Hidden Number Problem in Isabelle/HOL
Sage Binder, Eric Ren, Katherine Kosaian
- Formally verifying a vertical cell decomposition algorithm
Yves Bertot, Thomas Portet
- GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
Magnus O. Myreen, Mario Carneiro
- Hammering without ATPs (short paper)
Martin Desharnais, Jasmin Blanchette
- Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL
Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Andrew Reynolds, Jibiana Jakpor, Bruno Andreotti, Clark Barrett, Hans-Joerg Schurr, Cesare Tinelli
- LeanLTL: A unifying framework for linear temporal logics in Lean (Short Paper)
Eric Vin, Kyle Miller, Daniel J. Fremont
- Mechanising Böhm Trees and λη-Completeness
Chun Tian, Michael Norrish
- Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
Jérémy Thibault, Joseph Lenormand, Catalin Hritcu
- Nondeterministic Asynchronous Dataflow in Isabelle/HOL
Rafael Castro G. Silva, Laouen Fernet, Dmitriy Traytel
- Program Optimisations via Hylomorphisms for Extraction of Executable Code
David Castro Perez, Marco Paviotti, Michael Vollmer
- Scott’s Representation Theorem and the Univalent Karoubi Envelope
Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens
- Towards Automating Permutation Proofs in Coq: A Reflexive Approach with Iterative Deepening Search (Short Paper)
Nadeem Abdul Hamid
- Verification of the CVM algorithm with a Functional Probabilistic Invariant
Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan
- Verified Elimination of Secret Control-Flow
David Knothe, Oliver Bringmann
- Verifying an Efficient Algorithm for Computing Bernoulli Numbers
Manuel Eberl, Peter Lammich
- Verifying Datalog Reasoning with Lean
Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch
Organizers, sponsors and local information
See the shared pages of the colocated
conferences.
Last update 14 January 2025