default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID16th 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.
last updated on 2025-12-12 23:03 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
