| 2015 | HOCore in Coq. | Petar Maksimovic, Alan Schmitt |
| 2015 | Stream Fusion for Isabelle's Code Generator - Rough Diamond. | Andreas Lochbihler, Alexandra Maximova |
| 2015 | Refinement to Imperative/HOL. | Peter Lammich |
| 2015 | A Consistent Foundation for Isabelle/HOL. | Ondrej Kuncar, Andrei Popescu |
| 2015 | Learning to Parse on Aligned Corpora (Rough Diamond). | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | A Verified Enclosure for the Lorenz Attractor (Rough Diamond). | Fabian Immler |
| 2015 | A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. | Johannes Hlzl, Andreas Lochbihler, Dmitriy Traytel |
| 2015 | Improved Tool Support for Machine-Code Decompilation in HOL4. | Anthony C. J. Fox |
| 2015 | Proof-Producing Reflection for HOL - With an Application to Model Polymorphism. | Benja Fallenstein, Ramana Kumar |
| 2015 | Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker. | Lus Cruz-Filipe, Peter Schneider-Kamp |
| 2015 | Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. | Arthur Charguraud, Franois Pottier |
| 2015 | Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. | Hing-Lun Chan, Michael Norrish |
| 2015 | Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. | Sylvain Boulm, Alexandre Marchal |
| 2015 | Validating Dominator Trees for a Fast, Verified Dominance Test. | Sandrine Blazy, Delphine Demange, David Pichardie |
| 2015 | A Concrete Memory Model for CompCert. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2015 | Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. | Bruno Barras, Carst Tankink, Enrico Tassi |
| 2015 | ROSCoq: Robots Powered by Constructive Reals. | Abhishek Anand, Ross A. Knepper |
| 2015 | Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. | Reynald Affeldt, Jacques Garrigue |
| 2015 | Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
| 2014 | Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. | Makarius Wenzel |
| 2014 | Universe Polymorphism in Coq. | Matthieu Sozeau, Nicolas Tabareau |
| 2014 | On the Formalization of Z-Transform in HOL. | Umair Siddique, Mohamed Yousri Mahmoud, Sofine Tahar |
| 2014 | Collaborative Interactive Theorem Proving with Clide. | Martin Ring, Christoph Lth |
| 2014 | Mechanical Certification of Loop Pipelining Transformations: A Preview. | Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie |
| 2014 | Unified Decision Procedures for Regular Expression Equivalence. | Tobias Nipkow, Dmitriy Traytel |