| 2020 | A constructive formalization of the weak perfect graph theorem. Abhishek Kr Singh, Raja Natarajan |
| 2020 | A formal proof of the independence of the continuum hypothesis. Jesse Michael Han, Floris van Doorn |
| 2020 | A functional proof pearl: inverting the Ackermann hierarchy. Linh Tran, Anshuman Mohan, Aquinas Hobor |
| 2020 | A mechanized formalization of GraphQL. Tomás Díaz, Federico Olmedo, Éric Tanter |
| 2020 | A verified packrat parser interpreter for parsing expression grammars. Clement Blaudeau, Natarajan Shankar |
| 2020 | An equational theory for weak bisimulation via generalized parameterized coinduction. Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic |
| 2020 | Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. Christian Doczkal, Damien Pous |
| 2020 | ConCert: a smart contract certification framework in Coq. Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters |
| 2020 | Coq à la carte: a practical approach to modular syntax with binders. Yannick Forster, Kathrin Stark |
| 2020 | Cubical synthetic homotopy theory. Anders Mörtberg, Loïc Pujet |
| 2020 | Exploration of neural machine translation in autoformalization of mathematics in Mizar. Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban |
| 2020 | Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. David Butler, David Aspinall, Adrià Gascón |
| 2020 | Formalising perfectoid spaces. Kevin Buzzard, Johan Commelin, Patrick Massot |
| 2020 | Formalizing determinacy of concurrent revisions. Roy Overbeek |
| 2020 | Formalizing π-calculus in guarded cubical Agda. Niccolò Veltri, Andrea Vezzosi |
| 2020 | FreeSpec: specifying, verifying, and executing impure computations in Coq. Thomas Letan, Yann Régis-Gianas |
| 2020 | Frying the egg, roasting the chicken: unit deletions in DRAT proofs. Johannes Altmanninger, Adrian Rebola-Pardo |
| 2020 | Intrinsically-typed definitional interpreters for linear, session-typed languages. Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser |
| 2020 | Matching logic: the foundation of the K framework (invited talk). Grigore Rosu, Xiaohong Chen |
| 2020 | Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. Jasmin Blanchette, Catalin Hritcu |
| 2020 | Proof assistants at the hardware-software interface (invited talk). Adam Chlipala |
| 2020 | Proof pearl: Braun trees. Tobias Nipkow, Thomas Sewell |
| 2020 | REPLica: REPL instrumentation for Coq analysis. Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner |
| 2020 | The Poincaré-Bendixson theorem in Isabelle/HOL. Fabian Immler, Yong Kiam Tan |
| 2020 | The lean mathematical library. |
| 2020 | Three equivalent ordinal notation systems in cubical Agda. Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani |
| 2020 | Undecidability of higher-order unification formalised in Coq. Simon Spies, Yannick Forster |
| 2020 | Verified programming of Turing machines in Coq. Yannick Forster, Fabian Kunze, Maxi Wuttke |
| 2020 | Verified security of BLT signature scheme. Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja |
| 2020 | Verifying x86 instruction implementations. Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords |