| 2022 | (Deep) induction rules for GADTs. Patricia Johann, Enrico Ghiorzi |
| 2022 | A compositional proof framework for FRETish requirements. Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle |
| 2022 | A drag-and-drop proof tactic. Pablo Donato, Pierre-Yves Strub, Benjamin Werner |
| 2022 | A machine-checked direct proof of the Steiner-lehmus theorem. Ariel Kellison |
| 2022 | A verified algebraic representation of cairo program execution. Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
| 2022 | An extension of the framework types-to-sets for Isabelle/HOL. Mihails Milehins |
| 2022 | Applying formal verification to microkernel IPC at meta. Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli |
| 2022 | CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 Andrei Popescu, Steve Zdancewic |
| 2022 | CertiStr: a certified string solver. Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader |
| 2022 | Certified abstract machines for skeletal semantics. Guillaume Ambal, Sergueï Lenglet, Alan Schmitt |
| 2022 | Coq's vibrant ecosystem for verification engineering (invited talk). Andrew W. Appel |
| 2022 | Formal verification of a distributed dynamic reconfiguration protocol. William Schultz, Ian Dardik, Stavros Tripakis |
| 2022 | Formalising lie algebras. Oliver Nash |
| 2022 | Formally verified superblock scheduling. Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino |
| 2022 | Forward build systems, formally. Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt |
| 2022 | Implementing a category-theoretic framework for typed abstract syntax. Benedikt Ahrens, Ralph Matthes, Anders Mörtberg |
| 2022 | Mechanized verification of a fine-grained concurrent queue from meta's folly library. Simon Friis Vindum, Dan Frumin, Lars Birkedal |
| 2022 | On homotopy of walks and spherical maps in homotopy type theory. Jonathan Prieto-Cubides |
| 2022 | Overcoming restraint: composing verification of foreign functions with cogent. Louis Cheung, Liam O'Connor, Christine Rizkallah |
| 2022 | Reflection, rewinding, and coin-toss in EasyCrypt. Denis Firsov, Dominique Unruh |
| 2022 | Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting. Michael Färber |
| 2022 | Semantic cut elimination for the logic of bunched implications, formalized in Coq. Dan Frumin |
| 2022 | Specification and verification of a transient stack. Alexandre Moine, Arthur Charguéraud, François Pottier |
| 2022 | Structural embeddings revisited (invited talk). César Muñoz |
| 2022 | The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). June Andronick |
| 2022 | Undecidability, incompleteness, and completeness of second-order logic in Coq. Mark Koch, Dominik Kirst |
| 2022 | Verbatim++: verified, optimized, and semantically rich lexing with derivatives. Derek Egolf, Sam Lasser, Kathleen Fisher |
| 2022 | Windmills of the minds: an algorithm for fermat's two squares theorem. Hing-Lun Chan |