16th International Conference on Interactive Theorem Proving

ITP '25

Reykjavik, Iceland, 28 September-1 October 2025

part of FroCoS/ITP/TABLEAUX '25

News

The programme is out, see below!

The local policy prevents political statements in the presentation. ITP '25 will have a session dedicated to political discussion, and part of the business meeting will be dedicated to the place of political statements at ITP.

Accepted papers are out, see below!

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

• Kathrin Stark, Heriot-Watt University, Edinburgh, UK
• Laura Titolo, Code Metal

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

• 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

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.

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 regular (= non-reduced) 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.

The local policy prevents political statements in presentations. ITP '25 will have a session dedicated to political discussion, and part of the business meeting will be dedicated to the place of political statements at ITP.

Colocated workshops

Two workshops are colocated with ITP '25:

• Rocqshop on 27 September,
• ITP Lean Workshop on 2 October.

Programme committee cochairs

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

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
• Inductive Predicates via Least 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

Programme

Programme and registration

See the shared pages of the colocated conferences.

Organizers, sponsors and local information

See the shared pages of the colocated conferences.