| 2021 | 12th International Conference on Interactive Theorem Proving, ITP 2021, Rome, Italy (Virtual Conference), June 29 - July 1, 2021 Liron Cohen, Cezary Kaliszyk |
| 2021 | A Formal Proof of Modal Completeness for Provability Logic. Marco Maggesi, Cosimo Perini Brogi |
| 2021 | A Formalization of Dedekind Domains and Class Groups of Global Fields. Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio |
| 2021 | A Formally Verified Checker for First-Order Proofs. Seulkee Baek |
| 2021 | A Graphical User Interface Framework for Formal Verification. Edward W. Ayers, Mateja Jamnik, William T. Gowers |
| 2021 | A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. Yannick Forster, Fabian Kunze, Gert Smolka, Maxi Wuttke |
| 2021 | A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. Andreas Lochbihler |
| 2021 | A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. Adrian De Lon, Peter Koepke, Anton Lorenzen |
| 2021 | A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. Christian Doczkal |
| 2021 | A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. Katherine Cordwell, Yong Kiam Tan, André Platzer |
| 2021 | Bounded-Deducibility Security (Invited Paper). Andrei Popescu, Thomas Bauereiss, Peter Lammich |
| 2021 | Complete Bidirectional Typing for the Calculus of Inductive Constructions. Meven Lennon-Bertrand |
| 2021 | Flexible Coinduction in Agda. Luca Ciccone, Francesco Dagnino, Elena Zucca |
| 2021 | Formal Verification of Termination Criteria for First-Order Recursive Functions. César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, Thiago Mendonça Ferreira Ramos |
| 2021 | Formalising a Turing-Complete Choreographic Language in Coq. Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti |
| 2021 | Formalization of Basic Combinatorics on Words. Stepan Holub, Stepán Starosta |
| 2021 | Formalized Haar Measure. Floris van Doorn |
| 2021 | Front Matter, Table of Contents, Preface, Conference Organization. |
| 2021 | Homotopy Type Theory in Isabelle. Joshua Chen |
| 2021 | Itauto: An Extensible Intuitionistic SAT Solver. Frédéric Besson |
| 2021 | Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. Lennard Gäher, Fabian Kunze |
| 2021 | Proof Pearl : Playing with the Tower of Hanoi Formally. Laurent Théry |
| 2021 | Proving Quantum Programs Correct. Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks |
| 2021 | Reaching for the Star: Tale of a Monad in Coq. Pierre Nigron, Pierre-Évariste Dagand |
| 2021 | Specifying Message Formats with Contiguity Types. Konrad Slind |
| 2021 | Syntactic-Semantic Form of Mizar Articles. Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz |
| 2021 | Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). Nadia Polikarpova |
| 2021 | Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. Dominik Kirst, Marc Hermes |
| 2021 | The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). Magnus O. Myreen |
| 2021 | Unsolvability of the Quintic Formalized in Dependent Type Theory. Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub |
| 2021 | Value-Oriented Legal Argumentation in Isabelle/HOL. Christoph Benzmüller, David Fuenmayor |
| 2021 | Verified Double Sided Auctions for Financial Markets. Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh |
| 2021 | Verified Progress Tracking for Timely Dataflow. Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel |
| 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 |