| 2021 | CertRL: formalizing convergence proofs for value and policy iteration in Coq. | Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton |
| 2021 | A modular Isabelle framework for verifying saturation provers. | Sophie Tourret, Jasmin Blanchette |
| 2021 | Reasoning about monotonicity in separation logic. | Amin Timany, Lars Birkedal |
| 2021 | A formal proof of PAC learnability for decision stumps. | Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan |
| 2021 | Formal verification of semi-algebraic sets and real analytic functions. | J. Tanner Slagel, Lauren M. White, Aaron Dutle |
| 2021 | Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). | Peter Sewell |
| 2021 | Teaching algorithms and data structures with a proof assistant (invited talk). | Tobias Nipkow |
| 2021 | A minimalistic verified bootstrapped compiler (proof pearl). | Magnus O. Myreen |
| 2021 | Formal verification of authenticated, append-only skip lists in Agda. | Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. |
| 2021 | Lutsig: a verified Verilog compiler for verified circuit development. | Andreas Lw |
| 2021 | A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. | Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer |
| 2021 | A novice-friendly induction tactic for lean. | Jannis Limperg |
| 2021 | An anti-locally-nameless approach to formalizing quantifiers. | Olivier Laurent |
| 2021 | The generalised continuum hypothesis implies the axiom of choice in Coq. | Dominik Kirst, Felix Rech |
| 2021 | Formalizing category theory in Agda. | Jason Z. S. Hu, Jacques Carette |
| 2021 | Machine-checked semantic session typing. | Jonas Kastberg Hinrichsen, Danil Louwrink, Robbert Krebbers, Jesper Bengtson |
| 2021 | An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. | Max W. Haslbeck, Ren Thiemann |
| 2021 | Towards efficient and verified virtual machines for dynamic languages. | Martin Desharnais, Stefan Brunthaler |
| 2021 | Formalizing the ring of Witt vectors. | Johan Commelin, Robert Y. Lewis |
| 2021 | Towards formally verified compilation of tag-based policy enforcement. | Chris Chhak, Andrew Tolmach, Sean Noble Anderson |
| 2021 | On the formalisation of Kolmogorov complexity. | Elliot Catt, Michael Norrish |
| 2021 | A Coq formalization of data provenance. | Vronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rbecca Zucchini |
| 2021 | Developing and certifying Datalog optimizations in coq/mathcomp. | Pierre-Lo Bgay, Pierre Crgut, Jean-Franois Monin |
| 2021 | Lassie: HOL4 tactics by example. | Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar |
| 2021 | Extracting smart contracts tested and verified in Coq. | Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters |