default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID15th ITP 2024: Tbilisi, Georgia
- Yves Bertot
, Temur Kutsia, Michael Norrish:
15th International Conference on Interactive Theorem Proving, ITP 2024, Tbilisi, Georgia, September 9-14, 2024. LIPIcs 309, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024, ISBN 978-3-95977-337-9 - Front Matter, Table of Contents, Preface, Conference Organization. 0:i-0:xii
- Tobias Nipkow:
Alpha-Beta Pruning Verified (Invited Talk). 1:1-1:4 - Frédéric Blanqui:
Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk). 2:1-2:1 - Mohammad Abdulaziz, Thomas Ammer:
A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows. 3:1-3:19 - Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark:
Taming Differentiable Logics with Coq Formalisation. 4:1-4:19 - Reynald Affeldt, Zachary Stone:
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. 5:1-5:19 - Dagur Asgeirsson:
Towards Solid Abelian Groups: A Formal Proof of Nöbeling's Theorem. 6:1-6:17 - Benoît Ballenghien, Burkhart Wolff:
An Operational Semantics in Isabelle/HOL-CSP. 7:1-7:18 - Henning Basold, Peter Bruin, Dominique Lawson:
The Directed Van Kampen Theorem in Lean. 8:1-8:18 - Siddharth Bhat, Alex C. Keizer, Chris Hughes, Andrés Goens, Tobias Grosser:
Verifying Peephole Rewriting in SSA Compiler IRs. 9:1-9:20 - Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad:
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. 10:1-10:20 - Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincón:
A Formalization of the General Theory of Quaternions. 11:1-11:18 - Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret:
A Modular Formalization of Superposition in Isabelle/HOL. 12:1-12:20 - Burak Ekici, Nobuko Yoshida:
Completeness of Asynchronous Session Tree Subtyping in Coq. 13:1-13:20 - Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond:
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. 14:1-14:18 - Jacques Garrigue, Takafumi Saikawa:
Typed Compositional Quantum Computation with Lenses. 15:1-15:18 - Thibault Gauthier, Chad E. Brown:
A Formal Proof of R(4, 5)=25. 16:1-16:18 - Samuel Gruetter, Thomas Bourgeat, Adam Chlipala:
Verifying Software Emulation of an Unsupported Hardware Instruction. 17:1-17:16 - Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak:
Mechanized HOL Reasoning in Set Theory. 18:1-18:18 - Marc Hermes, Robbert Krebbers:
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. 19:1-19:18 - Dennis Hilhorst, Paige Randall North:
Formalizing the Algebraic Small Object Argument in UniMath. 20:1-20:18 - Michikazu Hirata:
A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL. 21:1-21:18 - Fabian Huch, Makarius Wenzel:
Distributed Parallel Build for the Isabelle Archive of Formal Proofs. 22:1-22:19 - Vincent Jackson, Toby Murray, Christine Rizkallah:
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. 23:1-23:16 - Dohan Kim:
An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility. 24:1-24:19 - Carl Kwan, Warren A. Hunt Jr.:
Formalizing the Cholesky Factorization Theorem. 25:1-25:16 - Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter:
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. 26:1-26:18 - Patrick Massot:
Teaching Mathematics Using Lean and Controlled Natural Language. 27:1-27:19 - Kai Obendrauf, Anne Baanen, Patrick Koopmann, Vera Stebletsova:
Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge. 28:1-28:18 - Karol Pak, Cezary Kaliszyk:
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. 29:1-29:18 - Sewon Park, Holger Thies:
A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. 30:1-30:19 - Martin Rau, Tobias Nipkow:
A Verified Earley Parser. 31:1-31:18 - Hannes Saffrich:
Abstractions for Multi-Sorted Substitutions. 32:1-32:19 - Audrey Seo, Christopher Lam, Dan Grossman, Talia Ringer:
Correctly Compiling Proofs About Programs Without Proving Compilers Correct. 33:1-33:20 - Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani:
Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics. 34:1-34:18 - Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule:
Formal Verification of the Empty Hexagon Number. 35:1-35:19 - Andrew Tolmach, Chris Chhak, Sean Noble Anderson:
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. 36:1-36:20 - Floris van Doorn, Heather Macbeth:
Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. 37:1-37:18 - Max Zeuner, Matthias Hutzler:
The Functor of Points Approach to Schemes in Cubical Agda. 38:1-38:18 - Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann:
Robust Mean Estimation by All Means (Short Paper). 39:1-39:8 - Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Formalising Half of a Graduate Textbook on Number Theory (Short Paper). 40:1-40:7 - Sam Ezeh:
Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). 41:1-41:8
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-04 22:07 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:
