| 2014 | Cardinals in Isabelle/HOL. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | A Formal Library for Elliptic Curves in the Coq Proof Assistant. | Evmorfia-Iro Bartzia, Pierre-Yves Strub |
| 2014 | A Heuristic Prover for Real Inequalities. | Jeremy Avigad, Robert Y. Lewis, Cody Roux |
| 2014 | HOL Constant Definition Done Right. | Rob Arthan |
| 2014 | Implicational Rewriting Tactics in HOL. | Vincent Aravantinos, Sofine Tahar |
| 2014 | Towards a Formally Verified Proof Assistant. | Abhishek Anand, Vincent Rahli |
| 2013 | Mechanising Turing Machines and Computability Theory in Isabelle/HOL. | Jian Xu, Xingyuan Zhang, Christian Urban |
| 2013 | Mechanical Verification of SAT Refutations with Extended Resolution. | Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr. |
| 2013 | Shared-Memory Multiprocessing for Interactive Theorem Proving. | Makarius Wenzel |
| 2013 | Adjustable References. | Viktor Vafeiadis |
| 2013 | Formalizing Bounded Increase. | Ren Thiemann |
| 2013 | Communicating Formal Proofs: The Case of Flyspeck. | Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers |
| 2013 | Certifying Voting Protocols. | Carsten Schrmann |
| 2013 | Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. | Vincent Rahli, Mark Bickford, Abhishek Anand |
| 2013 | A Parallelized Theorem Prover for a Logic with Parallel Execution. | David L. Rager, Warren A. Hunt Jr., Matt Kaufmann |
| 2013 | Kleene Algebra with Tests and Coq Tools for while Programs. | Damien Pous |
| 2013 | Automatically Generated Infrastructure for De Bruijn Syntaxes. | Emmanuel Polonowski |
| 2013 | Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. | Michael Norrish, Brian Huffman |
| 2013 | Square Root and Division Elimination in PVS. | Pierre Neron |
| 2013 | Steps towards Verified Implementations of HOL Light. | Magnus O. Myreen, Scott Owens, Ramana Kumar |
| 2013 | Handcrafted Inversions Made Operational on Operational Semantics. | Jean-Franois Monin, Xiaomu Shi |
| 2013 | Program Extraction from Nested Definitions. | Kenji Miyamoto, Fredrik Nordvall Forsberg, Helmut Schwichtenberg |
| 2013 | Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities. | Panagiotis Manolios |
| 2013 | The Picard Algorithm for Ordinary Differential Equations in Coq. | Evgeny Makarov, Bas Spitters |
| 2013 | Canonical Structures for the Working Coq User. | Assia Mahboubi, Enrico Tassi |