| 2021 | A Coq formalization of data provenance. Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini |
| 2021 | A formal proof of PAC learnability for decision stumps. Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan |
| 2021 | A minimalistic verified bootstrapped compiler (proof pearl). Magnus O. Myreen |
| 2021 | A modular Isabelle framework for verifying saturation provers. Sophie Tourret, Jasmin Blanchette |
| 2021 | A novice-friendly induction tactic for lean. Jannis Limperg |
| 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 | An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. Max W. Haslbeck, René Thiemann |
| 2021 | An anti-locally-nameless approach to formalizing quantifiers. Olivier Laurent |
| 2021 | CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021 Catalin Hritcu, Andrei Popescu |
| 2021 | CertRL: formalizing convergence proofs for value and policy iteration in Coq. Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton |
| 2021 | Contextual refinement of the Michael-Scott queue (proof pearl). Simon Friis Vindum, Lars Birkedal |
| 2021 | Developing and certifying Datalog optimizations in coq/mathcomp. Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin |
| 2021 | Extracting smart contracts tested and verified in Coq. Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters |
| 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 | Formal verification of semi-algebraic sets and real analytic functions. J. Tanner Slagel, Lauren M. White, Aaron Dutle |
| 2021 | Formalizing category theory in Agda. Jason Z. S. Hu, Jacques Carette |
| 2021 | Formalizing the ring of Witt vectors. Johan Commelin, Robert Y. Lewis |
| 2021 | Lassie: HOL4 tactics by example. Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar |
| 2021 | Lutsig: a verified Verilog compiler for verified circuit development. Andreas Lööw |
| 2021 | Machine-checked semantic session typing. Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson |
| 2021 | On the formalisation of Kolmogorov complexity. Elliot Catt, Michael Norrish |
| 2021 | Reasoning about monotonicity in separation logic. Amin Timany, Lars Birkedal |
| 2021 | Teaching algorithms and data structures with a proof assistant (invited talk). Tobias Nipkow |
| 2021 | The generalised continuum hypothesis implies the axiom of choice in Coq. Dominik Kirst, Felix Rech |
| 2021 | Towards efficient and verified virtual machines for dynamic languages. Martin Desharnais, Stefan Brunthaler |
| 2021 | Towards formally verified compilation of tag-based policy enforcement. Chris Chhak, Andrew Tolmach, Sean Noble Anderson |
| 2021 | Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). Peter Sewell |