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.
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
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.
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 a regular 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.
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
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 and registration
See the shared pages of the colocated
conferences.
Organizers, sponsors and local information
See the shared pages of the colocated
conferences.
