


default search action
16th ITP 2025: Reykjavik, Iceland
- Yannick Forster

, Chantal Keller
:
16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025. LIPIcs 352, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2025, ISBN 978-3-95977-396-6 - Front Matter, Table of Contents, Preface, Conference Organization. 0:i-0:xviii

- Remi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, Guy Katz:

A Certified Proof Checker for Deep Neural Network Verification in Imandra. 1:1-1:21 - Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa:

A Formal Analysis of Algorithms for Matroids and Greedoids. 2:1-2:19 - Jonas Bayer

, Marco David
:
A Formal Proof of Complexity Bounds on Diophantine Equations. 3:1-3:18 - Antoine Chambert-Loir

, María Inés de Frutos-Fernández:
A Formalization of Divided Powers in Lean. 4:1-4:17 - Joshua M. Cohen:

A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. 5:1-5:20 - Peter Koepke:

A Natural Language Formalization of Perfectoid Rings in ℕaproche. 6:1-6:15 - Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah:

A Verified Cost Model for Call-By-Push-Value. 7:1-7:19 - Asta Halkjær From, Anders Schlichtkrull:

Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting. 8:1-8:20 - Eric Wang, Arohee Bhoja, Cayden R. Codel, Noah G. Singer:

Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups. 9:1-9:19 - Dohan Kim

:
An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems. 10:1-10:20 - Jan van Brügge, Andrei Popescu

, Dmitriy Traytel:
Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. 11:1-11:20 - Anshula Gandhi, Anand Rao Tadipatri, Timothy Gowers:

Automatically Generalizing Proofs and Statements. 12:1-12:18 - Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs:

Barendregt's Theory of the λ-Calculus, Refreshed and Formalized. 13:1-13:22 - Chase Norman, Jeremy Avigad:

Canonical for Automated Theorem Proving in Lean. 14:1-14:20 - Elaine Li, Thomas Wies:

Certified Implementability of Global Multiparty Protocols. 15:1-15:20 - Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner:

Finiteness of Symbolic Derivatives in Lean. 16:1-16:19 - Stefania Damato

, Thorsten Altenkirch, Axel Ljungström:
Formalising Inductive and Coinductive Containers. 17:1-17:20 - Lawrence C. Paulson:

Formalising New Mathematics in Isabelle: Diagonal Ramsey. 18:1-18:18 - Burak Ekici

, Tadayoshi Kamegai, Nobuko Yoshida
:
Formalising Subject Reduction and Progress for Multiparty Session Processes. 19:1-19:23 - Mario Carneiro, Emily Riehl:

Formalizing Colimits in 𝒞at. 20:1-20:19 - Reynald Affeldt

, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa:
Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. 21:1-21:20 - Ghilain Bergeron, Florent Krasnopol, Sophie Tourret:

Formalizing Splitting in Isabelle/HOL. 22:1-22:19 - Sage Binder, Eric Ren, Katherine Kosaian:

Formalizing the Hidden Number Problem in Isabelle/HOL. 23:1-23:19 - Yves Bertot, Thomas Portet

:
Formally Verifying a Vertical Cell Decomposition Algorithm. 24:1-24:18 - Magnus O. Myreen, Mario Carneiro:

GOL in GOL in HOL: Verified Circuits in Conway's Game of Life. 25:1-25:18 - Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor

, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli:
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. 26:1-26:22 - Robbert Krebbers, Luko van der Maas

, Enrico Tassi:
Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. 27:1-27:21 - Chun Tian

, Michael Norrish
:
Mechanising Böhm Trees and λη-Completeness. 28:1-28:18 - Jérémy Thibault, Joseph Lenormand, Catalin Hritcu:

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs. 29:1-29:20 - Rafael Castro Gonçalves Silva, Laouen Fernet, Dmitriy Traytel:

Nondeterministic Asynchronous Dataflow in Isabelle/HOL. 30:1-30:20 - David Knothe, Oliver Bringmann:

On Verifying Secret Control Flow Elimination. 31:1-31:19 - David Castro-Perez, Marco Paviotti, Michael Vollmer:

Program Optimisations via Hylomorphisms for Extraction of Executable Code. 32:1-32:20 - Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens:

Scott's Representation Theorem and the Univalent Karoubi Envelope. 33:1-33:20 - Emin Karayel, Seng Joe Watt, Derek Khu

, Kuldeep S. Meel, Yong Kiam Tan:
Verification of the CVM Algorithm with a Functional Probabilistic Invariant. 34:1-34:20 - Manuel Eberl, Peter Lammich:

Verifying an Efficient Algorithm for Computing Bernoulli Numbers. 35:1-35:19 - Johannes Tantow

, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch:
Verifying Datalog Reasoning with Lean. 36:1-36:19 - Eric Vin

, Kyle A. Miller, Daniel J. Fremont:
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). 37:1-37:9 - Martin Desharnais, Jasmin Blanchette:

Sledgehammering Without ATPs (Short Paper). 38:1-38:8 - Nadeem Abdul Hamid

:
Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper). 39:1-39:7 - Kathrin Stark:

Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk). 40:1-40:2 - Laura Titolo:

Taming Floating-Point Rounding Errors with Proofs (Invited Talk). 41:1-41:3

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














