| 2021 | Formal Verification of Termination Criteria for First-Order Recursive Functions. | Csar A. Muoz, Mauricio Ayala-Rincn, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andria B. Avelar, Thiago Mendona Ferreira Ramos |
| 2021 | A Formal Proof of Modal Completeness for Provability Logic. | Marco Maggesi, Cosimo Perini Brogi |
| 2021 | A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. | Adrian De Lon, Peter Koepke, Anton Lorenzen |
| 2021 | A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. | Andreas Lochbihler |
| 2021 | Complete Bidirectional Typing for the Calculus of Inductive Constructions. | Meven Lennon-Bertrand |
| 2021 | Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. | Dominik Kirst, Marc Hermes |
| 2021 | Formalization of Basic Combinatorics on Words. | Stepan Holub, Stepn Starosta |
| 2021 | Proving Quantum Programs Correct. | Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks |
| 2021 | Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. | Lennard Gher, Fabian Kunze |
| 2021 | Formalized Haar Measure. | Floris van Doorn |
| 2021 | A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. | Christian Doczkal |
| 2021 | Formalising a Turing-Complete Choreographic Language in Coq. | Lus Cruz-Filipe, Fabrizio Montesi, Marco Peressotti |
| 2021 | A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. | Katherine Cordwell, Yong Kiam Tan, Andr Platzer |
| 2021 | Flexible Coinduction in Agda. | Luca Ciccone, Francesco Dagnino, Elena Zucca |
| 2021 | Homotopy Type Theory in Isabelle. | Joshua Chen |
| 2021 | Syntactic-Semantic Form of Mizar Articles. | Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz |
| 2021 | Itauto: An Extensible Intuitionistic SAT Solver. | Frdric Besson |
| 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 Benzmller, David Fuenmayor |
| 2021 | A Formally Verified Checker for First-Order Proofs. | Seulkee Baek |
| 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 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 | Verified Progress Tracking for Timely Dataflow. | Matthias Brun, Sra Decova, Andrea Lattuada, Dmitriy Traytel |
| 2021 | Bounded-Deducibility Security (Invited Paper). | Andrei Popescu, Thomas Bauereiss, Peter Lammich |