| 2022 | 13th International Conference on Interactive Theorem Proving, ITP 2022, Haifa, Israel, August 7-10, 2022 June Andronick, Leonardo de Moura |
| 2022 | A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). Jagadish Bapanapally, Ruben Gamboa |
| 2022 | A Verified Cyclicity Checker: For Theories with Overloaded Constants. Arve Gengelbach, Johannes Åman Pohjola |
| 2022 | Accelerating Verified-Compiler Development with a Verified Rewriting Engine. Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala |
| 2022 | Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala |
| 2022 | Candle: A Verified Implementation of HOL Light. Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell |
| 2022 | Compositional Verification of Interacting Systems Using Event Monads. Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia |
| 2022 | Computational Back-And-Forth Arguments in Constructive Type Theory. Dominik Kirst |
| 2022 | Dandelion: Certified Approximations of Elementary Functions. Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin |
| 2022 | Deeper Shallow Embeddings. Jacob Prinz, G. A. Kavvos, Leonidas Lampropoulos |
| 2022 | Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. Chelsea Edmonds, Lawrence C. Paulson |
| 2022 | Formalising Szemerédi's Regularity Lemma in Lean. Yaël Dillies, Bhavik Mehta |
| 2022 | Formalization of Randomized Approximation Algorithms for Frequency Moments. Emin Karayel |
| 2022 | Formalization of a Stochastic Approximation Theorem. Koundinya Vajjha, Barry M. Trager, Avraham Shinnar, Vasily Pestun |
| 2022 | Formalized functional analysis with semilinear maps. Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth |
| 2022 | Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu |
| 2022 | Formalizing a Diophantine Representation of the Set of Prime Numbers. Karol Pak, Cezary Kaliszyk |
| 2022 | Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. Yury Kudryashov |
| 2022 | Formalizing the Ring of Adèles of a Global Field. María Inés de Frutos-Fernández |
| 2022 | Front Matter, Table of Contents, Preface, Conference Organization. |
| 2022 | Kalas: A Verified, End-To-End Compiler for a Choreographic Language. Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish |
| 2022 | Mechanizing Soundness of Off-Policy Evaluation. Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas |
| 2022 | Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). Amy P. Felty |
| 2022 | Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant. Nicolas Magaud |
| 2022 | Refinement of Parallel Algorithms down to LLVM. Peter Lammich |
| 2022 | Reflexive Tactics for Algebra, Revisited. Kazuhiko Sakaguchi |
| 2022 | Seventeen Provers Under the Hammer. Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel |
| 2022 | Synthetic Kolmogorov Complexity in Coq. Yannick Forster, Fabian Kunze, Nils Lauermann |
| 2022 | Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen |
| 2022 | The Isabelle ENIGMA. Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban |
| 2022 | The Zoo of Lambda-Calculus Reduction Strategies, And Coq. Malgorzata Biernacka, Witold Charatonik, Tomasz Drab |
| 2022 | Undecidability of Dyadic First-Order Logic in Coq. Johannes Hostert, Andrej Dudenhefner, Dominik Kirst |
| 2022 | Use and Abuse of Instance Parameters in the Lean Mathematical Library. Anne Baanen |
| 2022 | User Interface Design in the HolPy Theorem Prover (Invited Talk). Bohua Zhan |
| 2022 | Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. Asta Halkjær From, Frederik Krogsdal Jacobsen |