| 2014 | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi |
| 2014 | A Coq Formalization of Finitely Presented Modules. Cyril Cohen, Anders Mörtberg |
| 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 | A New and Formalized Proof of Abstract Completion. Nao Hirokawa, Aart Middeldorp, Christian Sternagel |
| 2014 | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. Kento Emoto, Frédéric Loulergue, Julien Tesson |
| 2014 | An Isabelle Proof Method Language. Daniel Matichuk, Makarius Wenzel, Toby C. Murray |
| 2014 | Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK. Roderick Chapman, Florian Schanda |
| 2014 | Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. Makarius Wenzel |
| 2014 | Balancing Lists: A Proof Pearl. Guyslain Naves, Arnaud Spiwack |
| 2014 | Cardinals in Isabelle/HOL. Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | Collaborative Interactive Theorem Proving with Clide. Martin Ring, Christoph Lüth |
| 2014 | Completeness and Decidability Results for CTL in Coq. Christian Doczkal, Gert Smolka |
| 2014 | Compositional Computational Reflection. Gregory Malecha, Adam Chlipala, Thomas Braibant |
| 2014 | Experience Implementing a Performant Category-Theory Library in Coq. Jason Gross, Adam Chlipala, David I. Spivak |
| 2014 | Formal C Semantics: CompCert and the C Standard. Robbert Krebbers, Xavier Leroy, Freek Wiedijk |
| 2014 | Formal Verification of Optical Quantum Flip Gate. Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar |
| 2014 | Formalized, Effective Domain Theory in Coq. Robert Dockins |
| 2014 | From Operational Models to Information Theory; Side Channels in pGCL with Isabelle. David A. Cock |
| 2014 | HOL Constant Definition Done Right. Rob Arthan |
| 2014 | HOL with Definitions: Semantics, Soundness, and a Verified Implementation. Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens |
| 2014 | Hypermap Specification and Certified Linked Implementation Using Orbits. Jean-François Dufourd |
| 2014 | Implicational Rewriting Tactics in HOL. Vincent Aravantinos, Sofiène Tahar |
| 2014 | Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings Gerwin Klein, Ruben Gamboa |
| 2014 | Mechanical Certification of Loop Pipelining Transformations: A Preview. Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie |
| 2014 | Microcode Verification - Another Piece of the Microprocessor Verification Puzzle. Jared Davis, Anna Slobodová, Sol Swords |
| 2014 | On the Formalization of Z-Transform in HOL. Umair Siddique, Mohamed Yousri Mahmoud, Sofiène Tahar |
| 2014 | Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete. J Strother Moore |
| 2014 | Recursive Functions on Lazy Lists via Domains and Topologies. Andreas Lochbihler, Johannes Hölzl |
| 2014 | Rough Diamond: An Extension of Equivalence-Based Rewriting. Matt Kaufmann, J Strother Moore |
| 2014 | Showing Invariance Compositionally for a Process Algebra for Network Protocols. Timothy Bourke, Rob J. van Glabbeek, Peter Höfner |
| 2014 | The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It). Magnus O. Myreen, Jared Davis |
| 2014 | Towards a Formally Verified Proof Assistant. Abhishek Anand, Vincent Rahli |
| 2014 | Truly Modular (Co)datatypes for Isabelle/HOL. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel |
| 2014 | Unified Decision Procedures for Regular Expression Equivalence. Tobias Nipkow, Dmitriy Traytel |
| 2014 | Universe Polymorphism in Coq. Matthieu Sozeau, Nicolas Tabareau |
| 2014 | Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Sandrine Blazy, Vincent Laporte, David Pichardie |
| 2014 | Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. Peter Lammich |