| 2019 | Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. | Chad E. Brown, Cezary Kaliszyk, Karol Pak |
| 2019 | A Certificate-Based Approach to Formally Verified Approximations. | Florent Brhard, Assia Mahboubi, Damien Pous |
| 2019 | Primitive Floats in Coq. | Guillaume Bertholon, rik Martin-Dorel, Pierre Roux |
| 2019 | The DPRM Theorem in Isabelle (Short Paper). | Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher |
| 2019 | Data Types as Quotients of Polynomial Functors. | Jeremy Avigad, Mario Carneiro, Simon Hudon |
| 2019 | A Million Lines of Proof About a Moving Target (Invited Talk). | June Andronick |
| 2019 | Proving Tree Algorithms for Succinct Data Structures. | Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka |
| 2019 | A Verified Compositional Algorithm for AI Planning. | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
| 2019 | A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. | Yannick Forster, Fabian Kunze |
| 2019 | Complete Non-Orders and Fixed Points. | Akihisa Yamada, Jrmy Dubut |
| 2019 | A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. | Julian Brunner, Benedikt Seidl, Salomon Sickert |
| 2019 | First-Order Guarded Coinduction in Coq. | Lukasz Czajka |
| 2018 | An Agda Formalization of resin and Dubois' Asynchronous Fixed-Point Theory. | Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin |
| 2018 | Formalization of a Polymorphic Subtyping Algorithm. | Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers |
| 2018 | Verified Memoization and Dynamic Programming. | Simon Wimmer, Shuwei Hu, Tobias Nipkow |
| 2018 | MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). | Simon Wimmer, Johannes Hlzl |
| 2018 | Verified Tail Bounds for Randomized Programs. | Joseph Tassarotti, Robert Harper |
| 2018 | Program Verification in the Presence of Cached Address Translation. | Hira Taqdees Syeda, Gerwin Klein |
| 2018 | Formalizing Ring Theory in PVS. | Andria B. Avelar da Silva, Thaynara Arielly de Lima, Andr Luiz Galdino |
| 2018 | A Formal Equational Theory for Call-By-Push-Value. | Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic |
| 2018 | Towards Formal Foundations for Game Theory. | Julian Parsert, Cezary Kaliszyk |
| 2018 | Boosting the Reuse of Formal Specifications. | Mariano M. Moscato, Carlos Gustavo Lpez Pombo, Csar A. Muoz, Marco A. Feli |
| 2018 | Formalizing Implicative Algebras in Coq. | tienne Miquey |
| 2018 | A Formally Verified Solver for Homogeneous Linear Diophantine Equations. | Florian Mener, Julian Parsert, Jonas Schpf, Christian Sternagel |
| 2018 | Towards Verified Handwritten Calculational Proofs - (Short Paper). | Alexandra Mendes, Joo F. Ferreira |