| 2015 | A Concrete Memory Model for CompCert. Frédéric Besson, Sandrine Blazy, Pierre Wilke |
| 2015 | A Consistent Foundation for Isabelle/HOL. Ondrej Kuncar, Andrei Popescu |
| 2015 | A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel |
| 2015 | A Linear First-Order Functional Intermediate Language for Verified Compilers. Sigurd Schneider, Gert Smolka, Sebastian Hack |
| 2015 | A Mechanized Theory of Regular Trees in Dependent Type Theory. Régis Spadotti |
| 2015 | A Verified Enclosure for the Lorenz Attractor (Rough Diamond). Fabian Immler |
| 2015 | Affine Arithmetic and Applications to Real-Number Proving. Mariano M. Moscato, César A. Muñoz, Andrew P. Smith |
| 2015 | Amortized Complexity Verified. Tobias Nipkow |
| 2015 | Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. Bruno Barras, Carst Tankink, Enrico Tassi |
| 2015 | Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. Steven Schäfer, Tobias Tebbi, Gert Smolka |
| 2015 | Deriving Comparators and Show Functions in Isabelle/HOL. Christian Sternagel, René Thiemann |
| 2015 | Formalising Knot Theory in Isabelle/HOL. T. V. H. Prathamesh |
| 2015 | Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. Reynald Affeldt, Jacques Garrigue |
| 2015 | Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker. Luís Cruz-Filipe, Peter Schneider-Kamp |
| 2015 | Foundational Property-Based Testing. Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce |
| 2015 | HOCore in Coq. Petar Maksimovic, Alan Schmitt |
| 2015 | Improved Tool Support for Machine-Code Decompilation in HOL4. Anthony C. J. Fox |
| 2015 | Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings Christian Urban, Xingyuan Zhang |
| 2015 | Learning to Parse on Aligned Corpora (Rough Diamond). Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
| 2015 | Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. Arthur Charguéraud, François Pottier |
| 2015 | Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. Hing-Lun Chan, Michael Norrish |
| 2015 | ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. Filip Sieczkowski, Ales Bizjak, Lars Birkedal |
| 2015 | Pattern Matches in HOL: - A New Representation and Improved Code Generation. Thomas Tuerk, Magnus O. Myreen, Ramana Kumar |
| 2015 | Proof-Producing Reflection for HOL - With an Application to Model Polymorphism. Benja Fallenstein, Ramana Kumar |
| 2015 | ROSCoq: Robots Powered by Constructive Reals. Abhishek Anand, Ross A. Knepper |
| 2015 | Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal |
| 2015 | Refinement to Imperative/HOL. Peter Lammich |
| 2015 | Stream Fusion for Isabelle's Code Generator - Rough Diamond. Andreas Lochbihler, Alexandra Maximova |
| 2015 | Transfinite Constructions in Classical Type Theory. Gert Smolka, Steven Schäfer, Christian Doczkal |
| 2015 | Validating Dominator Trees for a Fast, Verified Dominance Test. Sandrine Blazy, Delphine Demange, David Pichardie |
| 2015 | Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. Mohammad Abdulaziz, Charles Gretton, Michael Norrish |