| 2023 | Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. | Ana de Almeida Borges, Annal Casanueva Arts, Jean-Rmy Falleri, Emilio Jess Gallego Arias, rik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Tho Zimmermann |
| 2023 | Fermat's Last Theorem for Regular Primes (Short Paper). | Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi |
| 2023 | A Proof-Producing Compiler for Blockchain Applications. | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
| 2023 | An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. | David Kurniadi Angdinata, Junyan Xu |
| 2023 | Formalizing Functions as Processes. | Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen |
| 2023 | Fast, Verified Computation for Candle. | Oskar Abrahamsson, Magnus O. Myreen |
| 2023 | A Formal Analysis of RANKING. | Mohammad Abdulaziz, Christoph Madlener |
| 2023 | Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). | Akihisa Yamada, Jrmy Dubut |
| 2022 | Compositional Verification of Interacting Systems Using Event Monads. | Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia |
| 2022 | User Interface Design in the HolPy Theorem Prover (Invited Talk). | Bohua Zhan |
| 2022 | Mechanizing Soundness of Off-Policy Evaluation. | Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas |
| 2022 | Front Matter, Table of Contents, Preface, Conference Organization. | |
| 2022 | Formalization of a Stochastic Approximation Theorem. | Koundinya Vajjha, Barry M. Trager, Avraham Shinnar, Vasily Pestun |
| 2022 | Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. | Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu |
| 2022 | Reflexive Tactics for Algebra, Revisited. | Kazuhiko Sakaguchi |
| 2022 | Deeper Shallow Embeddings. | Jacob Prinz, G. A. Kavvos, Leonidas Lampropoulos |
| 2022 | Kalas: A Verified, End-To-End Compiler for a Choreographic Language. | Johannes man Pohjola, Alejandro Gmez-Londoo, James Shaker, Michael Norrish |
| 2022 | Formalizing a Diophantine Representation of the Set of Prime Numbers. | Karol Pak, Cezary Kaliszyk |
| 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 | Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. | Yury Kudryashov |
| 2022 | Computational Back-And-Forth Arguments in Constructive Type Theory. | Dominik Kirst |
| 2022 | Formalization of Randomized Approximation Algorithms for Frequency Moments. | Emin Karayel |
| 2022 | Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. | Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen |
| 2022 | Undecidability of Dyadic First-Order Logic in Coq. | Johannes Hostert, Andrej Dudenhefner, Dominik Kirst |