| 2020 | An equational theory for weak bisimulation via generalized parameterized coinduction. | Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic |
| 2020 | The lean mathematical library. | |
| 2020 | Exploration of neural machine translation in autoformalization of mathematics in Mizar. | Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban |
| 2020 | Formalizing π-calculus in guarded cubical Agda. | Niccol Veltri, Andrea Vezzosi |
| 2020 | A functional proof pearl: inverting the Ackermann hierarchy. | Linh Tran, Anshuman Mohan, Aquinas Hobor |
| 2020 | Undecidability of higher-order unification formalised in Coq. | Simon Spies, Yannick Forster |
| 2020 | A constructive formalization of the weak perfect graph theorem. | Abhishek Kr Singh, Raja Natarajan |
| 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 | REPLica: REPL instrumentation for Coq analysis. | Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner |
| 2020 | Formalizing determinacy of concurrent revisions. | Roy Overbeek |
| 2020 | Proof pearl: Braun trees. | Tobias Nipkow, Thomas Sewell |
| 2020 | Cubical synthetic homotopy theory. | Anders Mrtberg, Loc Pujet |
| 2020 | FreeSpec: specifying, verifying, and executing impure computations in Coq. | Thomas Letan, Yann Rgis-Gianas |
| 2020 | The Poincar-Bendixson theorem in Isabelle/HOL. | Fabian Immler, Yong Kiam Tan |
| 2020 | A formal proof of the independence of the continuum hypothesis. | Jesse Michael Han, Floris van Doorn |
| 2020 | Verifying x86 instruction implementations. | Shilpi Goel, Anna Slobodov, Rob Sumners, Sol Swords |
| 2020 | Three equivalent ordinal notation systems in cubical Agda. | Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani |
| 2020 | Verified security of BLT signature scheme. | Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja |
| 2020 | Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. | Christian Doczkal, Damien Pous |
| 2020 | A mechanized formalization of GraphQL. | Toms Daz, Federico Olmedo, ric Tanter |
| 2020 | Proof assistants at the hardware-software interface (invited talk). | Adam Chlipala |
| 2020 | Formalising perfectoid spaces. | Kevin Buzzard, Johan Commelin, Patrick Massot |
| 2020 | A verified packrat parser interpreter for parsing expression grammars. | Clement Blaudeau, Natarajan Shankar |
| 2020 | ConCert: a smart contract certification framework in Coq. | Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters |