| 2022 | Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. | Jason Gross, Tho Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala |
| 2022 | Accelerating Verified-Compiler Development with a Verified Rewriting Engine. | Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala |
| 2022 | The Isabelle ENIGMA. | Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsk, Jelle Piepenbrock, Josef Urban |
| 2022 | A Verified Cyclicity Checker: For Theories with Overloaded Constants. | Arve Gengelbach, Johannes man Pohjola |
| 2022 | Formalizing the Ring of Adles of a Global Field. | Mara Ins de Frutos-Fernndez |
| 2022 | Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. | Asta Halkjr From, Frederik Krogsdal Jacobsen |
| 2022 | Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). | Amy P. Felty |
| 2022 | Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. | Chelsea Edmonds, Lawrence C. Paulson |
| 2022 | Formalized functional analysis with semilinear maps. | Frdric Dupuis, Robert Y. Lewis, Heather Macbeth |
| 2022 | Formalising Szemerdi's Regularity Lemma in Lean. | Yal Dillies, Bhavik Mehta |
| 2022 | Seventeen Provers Under the Hammer. | Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel |
| 2022 | The Zoo of Lambda-Calculus Reduction Strategies, And Coq. | Malgorzata Biernacka, Witold Charatonik, Tomasz Drab |
| 2022 | Dandelion: Certified Approximations of Elementary Functions. | Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin |
| 2022 | A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). | Jagadish Bapanapally, Ruben Gamboa |
| 2022 | Use and Abuse of Instance Parameters in the Lean Mathematical Library. | Anne Baanen |
| 2022 | Candle: A Verified Implementation of HOL Light. | Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell |
| 2022 | Synthetic Kolmogorov Complexity in Coq. | Yannick Forster, Fabian Kunze, Nils Lauermann |
| 2021 | Verifying an HTTP Key-Value Server with Interaction Trees and VST. | Hengchu Zhang, Wolf Honor, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic |
| 2021 | Front Matter, Table of Contents, Preface, Conference Organization. | |
| 2021 | Proof Pearl : Playing with the Tower of Hanoi Formally. | Laurent Thry |
| 2021 | Specifying Message Formats with Contiguity Types. | Konrad Slind |
| 2021 | Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). | Nadia Polikarpova |
| 2021 | Reaching for the Star: Tale of a Monad in Coq. | Pierre Nigron, Pierre-variste Dagand |
| 2021 | Verified Double Sided Auctions for Financial Markets. | Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh |
| 2021 | The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). | Magnus O. Myreen |