| 2014 | Balancing Lists: A Proof Pearl. | Guyslain Naves, Arnaud Spiwack |
| 2014 | The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It). | Magnus O. Myreen, Jared Davis |
| 2014 | Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete. | J Strother Moore |
| 2014 | An Isabelle Proof Method Language. | Daniel Matichuk, Makarius Wenzel, Toby C. Murray |
| 2014 | Compositional Computational Reflection. | Gregory Malecha, Adam Chlipala, Thomas Braibant |
| 2014 | Formal Verification of Optical Quantum Flip Gate. | Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofine Tahar |
| 2014 | Recursive Functions on Lazy Lists via Domains and Topologies. | Andreas Lochbihler, Johannes Hlzl |
| 2014 | Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. | Peter Lammich |
| 2014 | HOL with Definitions: Semantics, Soundness, and a Verified Implementation. | Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens |
| 2014 | Formal C Semantics: CompCert and the C Standard. | Robbert Krebbers, Xavier Leroy, Freek Wiedijk |
| 2014 | Rough Diamond: An Extension of Equivalence-Based Rewriting. | Matt Kaufmann, J Strother Moore |
| 2014 | A New and Formalized Proof of Abstract Completion. | Nao Hirokawa, Aart Middeldorp, Christian Sternagel |
| 2014 | Experience Implementing a Performant Category-Theory Library in Coq. | Jason Gross, Adam Chlipala, David I. Spivak |
| 2014 | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. | Kento Emoto, Frdric Loulergue, Julien Tesson |
| 2014 | Hypermap Specification and Certified Linked Implementation Using Orbits. | Jean-Franois Dufourd |
| 2014 | Completeness and Decidability Results for CTL in Coq. | Christian Doczkal, Gert Smolka |
| 2014 | Formalized, Effective Domain Theory in Coq. | Robert Dockins |
| 2014 | Microcode Verification - Another Piece of the Microprocessor Verification Puzzle. | Jared Davis, Anna Slobodov, Sol Swords |
| 2014 | A Coq Formalization of Finitely Presented Modules. | Cyril Cohen, Anders Mrtberg |
| 2014 | From Operational Models to Information Theory; Side Channels in pGCL with Isabelle. | David A. Cock |
| 2014 | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). | Frdric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi |
| 2014 | Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK. | Roderick Chapman, Florian Schanda |
| 2014 | Showing Invariance Compositionally for a Process Algebra for Network Protocols. | Timothy Bourke, Rob J. van Glabbeek, Peter Hfner |
| 2014 | Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. | Sandrine Blazy, Vincent Laporte, David Pichardie |
| 2014 | Truly Modular (Co)datatypes for Isabelle/HOL. | Jasmin Christian Blanchette, Johannes Hlzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel |