| 2025 | 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025 Yannick Forster, Chantal Keller |
| 2025 | A Certified Proof Checker for Deep Neural Network Verification in Imandra. Remi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, Guy Katz |
| 2025 | A Formal Analysis of Algorithms for Matroids and Greedoids. Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa |
| 2025 | A Formal Proof of Complexity Bounds on Diophantine Equations. Jonas Bayer, Marco David |
| 2025 | A Formalization of Divided Powers in Lean. Antoine Chambert-Loir, María Inés de Frutos-Fernández |
| 2025 | A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. Joshua M. Cohen |
| 2025 | A Natural Language Formalization of Perfectoid Rings in ℕaproche. Peter Koepke |
| 2025 | A Verified Cost Model for Call-By-Push-Value. Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah |
| 2025 | Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting. Asta Halkjær From, Anders Schlichtkrull |
| 2025 | Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups. Eric Wang, Arohee Bhoja, Cayden R. Codel, Noah G. Singer |
| 2025 | An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems. Dohan Kim |
| 2025 | Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. Jan van Brügge, Andrei Popescu, Dmitriy Traytel |
| 2025 | Automatically Generalizing Proofs and Statements. Anshula Gandhi, Anand Rao Tadipatri, Timothy Gowers |
| 2025 | Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk). Kathrin Stark |
| 2025 | Barendregt's Theory of the λ-Calculus, Refreshed and Formalized. Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs |
| 2025 | Canonical for Automated Theorem Proving in Lean. Chase Norman, Jeremy Avigad |
| 2025 | Certified Implementability of Global Multiparty Protocols. Elaine Li, Thomas Wies |
| 2025 | Finiteness of Symbolic Derivatives in Lean. Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner |
| 2025 | Formalising Inductive and Coinductive Containers. Stefania Damato, Thorsten Altenkirch, Axel Ljungström |
| 2025 | Formalising New Mathematics in Isabelle: Diagonal Ramsey. Lawrence C. Paulson |
| 2025 | Formalising Subject Reduction and Progress for Multiparty Session Processes. Burak Ekici, Tadayoshi Kamegai, Nobuko Yoshida |
| 2025 | Formalizing Colimits in 𝒞at. Mario Carneiro, Emily Riehl |
| 2025 | Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa |
| 2025 | Formalizing Splitting in Isabelle/HOL. Ghilain Bergeron, Florent Krasnopol, Sophie Tourret |
| 2025 | Formalizing the Hidden Number Problem in Isabelle/HOL. Sage Binder, Eric Ren, Katherine Kosaian |
| 2025 | Formally Verifying a Vertical Cell Decomposition Algorithm. Yves Bertot, Thomas Portet |
| 2025 | Front Matter, Table of Contents, Preface, Conference Organization. |
| 2025 | GOL in GOL in HOL: Verified Circuits in Conway's Game of Life. Magnus O. Myreen, Mario Carneiro |
| 2025 | Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli |
| 2025 | Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. Robbert Krebbers, Luko van der Maas, Enrico Tassi |
| 2025 | LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). Eric Vin, Kyle A. Miller, Daniel J. Fremont |
| 2025 | Mechanising Böhm Trees and λη-Completeness. Chun Tian, Michael Norrish |
| 2025 | Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs. Jérémy Thibault, Joseph Lenormand, Catalin Hritcu |
| 2025 | Nondeterministic Asynchronous Dataflow in Isabelle/HOL. Rafael Castro Gonçalves Silva, Laouen Fernet, Dmitriy Traytel |
| 2025 | On Verifying Secret Control Flow Elimination. David Knothe, Oliver Bringmann |
| 2025 | Program Optimisations via Hylomorphisms for Extraction of Executable Code. David Castro-Perez, Marco Paviotti, Michael Vollmer |
| 2025 | Scott's Representation Theorem and the Univalent Karoubi Envelope. Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens |
| 2025 | Sledgehammering Without ATPs (Short Paper). Martin Desharnais, Jasmin Blanchette |
| 2025 | Taming Floating-Point Rounding Errors with Proofs (Invited Talk). Laura Titolo |
| 2025 | Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper). Nadeem Abdul Hamid |
| 2025 | Verification of the CVM Algorithm with a Functional Probabilistic Invariant. Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan |
| 2025 | Verifying Datalog Reasoning with Lean. Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch |
| 2025 | Verifying an Efficient Algorithm for Computing Bernoulli Numbers. Manuel Eberl, Peter Lammich |