ITP

Publications

2023

Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, Talia Ringer
Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. ITP (2023)
María Inés de Frutos-Fernández
Formalizing Norm Extensions and Applications to Number Theory. ITP (2023)
Amelia Livingston
Group Cohomology in the Lean Community Library. ITP (2023)
Jujian Zhang
Formalising the Proj Construction in Lean. ITP (2023)
Yiming Xu, Michael Norrish
Dependently Sorted Theorem Proving for Mathematical Foundations. ITP (2023)
Dominique Larchey-Wendling, Jean-François Monin
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. ITP (2023)
Philipp Joram, Niccolò Veltri
Constructive Final Semantics of Finite Bags. ITP (2023)
Christina Kohl, Aart Middeldorp
Formalizing Almost Development Closed Critical Pairs (Short Paper). ITP (2023)
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
MizAR 60 for Mizar 50. ITP (2023)
Chengsong Tan, Christian Urban
POSIX Lexing with Bitcoded Derivatives. ITP (2023)
Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. ITP (2023)
Roger Bosman, Georgios Karachalias, Tom Schrijvers
No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. ITP (2023)
Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi
Fermat's Last Theorem for Regular Primes (Short Paper). ITP (2023)
Niels van der Weide, Deivid Vale, Cynthia Kop
Certifying Higher-Order Polynomial Interpretations. ITP (2023)
Balázs Tóth, Tobias Nipkow
Real-Time Double-Ended Queue Verified (Proof Pearl). ITP (2023)
Mario Carneiro, Chad E. Brown, Josef Urban
Automated Theorem Proving for Metamath. ITP (2023)
Oliver Nash
A Formalisation of Gallagher's Ergodic Theorem. ITP (2023)
Akihisa Yamada, Jérémy Dubut
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). ITP (2023)
Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone
A Sound and Complete Projection for Global Types. ITP (2023)
Luís Cruz-Filipe, Fabrizio Montesi
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. ITP (2023)
Jarl G. Taxerås Flaten
Formalising Yoneda Ext in Univalent Foundations. ITP (2023)
Mario Carneiro
Reimplementing Mizar in Rust. ITP (2023)
Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. ITP (2023)
Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
LISA - A Modern Proof System. ITP (2023)
Angeliki Koutsoukou-Argyraki
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). ITP (2023)
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)
Martin Dvorak, Jasmin Blanchette
Closure Properties of General Grammars - Formally Verified. ITP (2023)
Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen
Formalizing Functions as Processes. ITP (2023)
Niels F. W. Voorneveld
Slice Nondeterminism. ITP (2023)
Lawrence Dunn, Val Tannen, Steve Zdancewic
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. ITP (2023)
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
A Proof-Producing Compiler for Blockchain Applications. ITP (2023)
Adam Grabowski, Artur Kornilowicz
Implementing More Explicit Definitional Expansions in Mizar (Short Paper). ITP (2023)
Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel
Foundational Verification of Stateful P4 Packet Processing. ITP (2023)
Robbert Krebbers
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). ITP (2023)
Mohammad Abdulaziz, Christoph Madlener
A Formal Analysis of RANKING. ITP (2023)
Front Matter, Table of Contents, Preface, Conference Organization. ITP (2023)
Oskar Abrahamsson, Magnus O. Myreen
Fast, Verified Computation for Candle. ITP (2023)
Wojciech Nawrocki, Edward W. Ayers, Gabriel Ebner
An Extensible User Interface for Lean 4. ITP (2023)
David Kurniadi Angdinata, Junyan Xu
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. ITP (2023)

volume 268, 2023

14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland ITP 268 (2023)

2022

volume 237, 2022

13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel. ITP 237 (2022)