- Patrick Massot:
Teaching Mathematics Using Lean and Controlled Natural Language. ITP 2024: 27:1-27:19 - Tobias Nipkow:
Alpha-Beta Pruning Verified (Invited Talk). ITP 2024: 1:1-1:4 - Kai Obendrauf, Anne Baanen, Patrick Koopmann, Vera Stebletsova:
Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge. ITP 2024: 28:1-28:18 - Karol Pak, Cezary Kaliszyk:
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. ITP 2024: 29:1-29:18 - Martin Rau, Tobias Nipkow:
A Verified Earley Parser. ITP 2024: 31:1-31:18 - Hannes Saffrich:
Abstractions for Multi-Sorted Substitutions. ITP 2024: 32:1-32:19 - Audrey Seo, Christopher Lam, Dan Grossman, Talia Ringer:
Correctly Compiling Proofs About Programs Without Proving Compilers Correct. ITP 2024: 33:1-33:20 - Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani:
Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics. ITP 2024: 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. ITP 2024: 35:1-35:19 - Andrew Tolmach, Chris Chhak, Sean Noble Anderson:
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. ITP 2024: 36:1-36:20 - Front Matter, Table of Contents, Preface, Conference Organization. ITP 2024: 0:i-0:xii
- Max Zeuner, Matthias Hutzler:
The Functor of Points Approach to Schemes in Cubical Agda. ITP 2024: 38:1-38:18 - Yves Bertot
, Temur Kutsia, Michael Norrish:
15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia. LIPIcs 309, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024, ISBN 978-3-95977-337-9 [contents] - 2023
- Akihisa Yamada, Jérémy Dubut:
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). ITP 2023: 34:1-34:13 - Mohammad Abdulaziz, Christoph Madlener:
A Formal Analysis of RANKING. ITP 2023: 3:1-3:18 - Oskar Abrahamsson, Magnus O. Myreen:
Fast, Verified Computation for Candle. ITP 2023: 4:1-4:17 - Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen:
Formalizing Functions as Processes. ITP 2023: 5:1-5:21 - David Kurniadi Angdinata, Junyan Xu:
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. ITP 2023: 6:1-6:19 - Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman:
A Proof-Producing Compiler for Blockchain Applications. ITP 2023: 7:1-7:19 - Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi:
Fermat's Last Theorem for Regular Primes (Short Paper). ITP 2023: 36:1-36:8 - Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann:
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. ITP 2023: 12:1-12:18 - Roger Bosman, Georgios Karachalias, Tom Schrijvers:
No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. ITP 2023: 8:1-8:18 - Mario Carneiro:
Reimplementing Mizar in Rust. ITP 2023: 10:1-10:18 - Mario Carneiro, Chad E. Brown, Josef Urban:
Automated Theorem Proving for Metamath. ITP 2023: 9:1-9:19 - Luís Cruz-Filipe, Fabrizio Montesi:
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. ITP 2023: 11:1-11:19 - Lawrence Dunn, Val Tannen, Steve Zdancewic:
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. ITP 2023: 14:1-14:20 - Martin Dvorak, Jasmin Blanchette:
Closure Properties of General Grammars - Formally Verified. ITP 2023: 15:1-15:16 - Jarl G. Taxerås Flaten:
Formalising Yoneda Ext in Univalent Foundations. ITP 2023: 16:1-16:17 - María Inés de Frutos-Fernández:
Formalizing Norm Extensions and Applications to Number Theory. ITP 2023: 13:1-13:18 - Adam Grabowski, Artur Kornilowicz:
Implementing More Explicit Definitional Expansions in Mizar (Short Paper). ITP 2023: 37:1-37:8
