| 2011 | The Web of Mathematical Models: A Schema-based, Wiki-like, Interactive Platform. | Thomas Grundmann, Jean-Marie Gaillourdet, Karsten Schmidt, Arnd Poetzsch-Heffter, Stefan Deloch, Martin Memmel |
| 2011 | Point-Free, Set-Free Concrete Linear Algebra. | Georges Gonthier |
| 2011 | Advances in the Formalization of the Odd Order Theorem. | Georges Gonthier |
| 2011 | Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. | Peter Gammie |
| 2011 | LCF-Style Bit-Blasting in HOL4. | Anthony C. J. Fox |
| 2011 | A Linear Algebra Wiki. | Michael Doob |
| 2011 | The PlanetMath Encyclopedia. | Joseph Corneli |
| 2011 | Towards Robustness Analysis Using PVS. | Renaud Clavel, Laurence Pierre, Rgis Leveugle |
| 2011 | Structural Analysis of Narratives with the Coq Proof Assistant. | Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza |
| 2011 | Relational Decomposition. | Lennart Beringer |
| 2011 | Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. | Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal |
| 2011 | Towards Verification of Product Lines. | Don S. Batory |
| 2011 | Metadata for a wiki of formalized mathematics. | Jesse Alama |
| 2010 | Validating QBF Invalidity in HOL4. | Tjark Weber |
| 2010 | Inductive Consequences in the Calculus of Constructions. | Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
| 2010 | A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. | Freek Verbeek, Julien Schmaltz |
| 2010 | Antifounded Coinduction in Type Theory. | Tarmo Uustalu |
| 2010 | A Mechanically Verified AIG-to-BDD Conversion Algorithm. | Sol Swords, Warren A. Hunt Jr. |
| 2010 | Termination Casts: A Flexible Approach to Termination with General Recursion. | Aaron Stump, Vilhelm Sjberg, Stephanie Weirich |
| 2010 | Developing the Algebraic Hierarchy with Type Classes in Coq. | Bas Spitters, Eelis van der Weegen |
| 2010 | Equations: A Dependent Pattern-Matching Compiler. | Matthieu Sozeau |
| 2010 | Proof Assistants as Teaching Assistants: A View from the Trenches. | Benjamin C. Pierce |
| 2010 | Separation Logic Adapted for Proofs by Rewriting. | Magnus O. Myreen |
| 2010 | On the Formalization of the Lebesgue Integration Theory in HOL. | Tarek Mhamdi, Osman Hasan, Sofine Tahar |
| 2010 | Cyclic Proofs and Coinductive Principles. | Gavin Mendel-Gleason, Geoff W. Hamilton |