| 2013 | A Machine-Checked Proof of the Odd Order Theorem. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry |
| 2013 | A Parallelized Theorem Prover for a Logic with Parallel Execution. David L. Rager, Warren A. Hunt Jr., Matt Kaufmann |
| 2013 | Adjustable References. Viktor Vafeiadis |
| 2013 | Applying Formal Methods in the Large. Dominique Bolignano |
| 2013 | Automatic Data Refinement. Peter Lammich |
| 2013 | Automatically Generated Infrastructure for De Bruijn Syntaxes. Emmanuel Polonowski |
| 2013 | Automating Theorem Proving with SMT. K. Rustan M. Leino |
| 2013 | Canonical Structures for the Working Coq User. Assia Mahboubi, Enrico Tassi |
| 2013 | Certifying Voting Protocols. Carsten Schürmann |
| 2013 | Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. Jörg Endrullis, Dimitri Hendriks, Martin Bodin |
| 2013 | Communicating Formal Proofs: The Case of Flyspeck. Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers |
| 2013 | Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities. Panagiotis Manolios |
| 2013 | Data Refinement in Isabelle/HOL. Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow |
| 2013 | Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. Vincent Rahli, Mark Bickford, Abhishek Anand |
| 2013 | Formal Reasoning about Classified Markov Chains in HOL. Liya Liu, Osman Hasan, Vincent Aravantinos, Sofiène Tahar |
| 2013 | Formalizing Bounded Increase. René Thiemann |
| 2013 | Handcrafted Inversions Made Operational on Operational Semantics. Jean-François Monin, Xiaomu Shi |
| 2013 | Implementing Hash-Consed Structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
| 2013 | Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings Sandrine Blazy, Christine Paulin-Mohring, David Pichardie |
| 2013 | Kleene Algebra with Tests and Coq Tools for while Programs. Damien Pous |
| 2013 | Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. Andreas Lochbihler |
| 2013 | Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. Guillaume Claret, Lourdes Del Carmen González-Huesca, Yann Régis-Gianas, Beta Ziliani |
| 2013 | MaSh: Machine Learning for Sledgehammer. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban |
| 2013 | Mechanical Verification of SAT Refutations with Extended Resolution. Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr. |
| 2013 | Mechanising Turing Machines and Computability Theory in Isabelle/HOL. Jian Xu, Xingyuan Zhang, Christian Urban |
| 2013 | Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. Michael Norrish, Brian Huffman |
| 2013 | Practical Probability: Applying pGCL to Lattice Scheduling. David A. Cock |
| 2013 | Pragmatic Quotient Types in Coq. Cyril Cohen |
| 2013 | Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. Alasdair Armstrong, Georg Struth, Tjark Weber |
| 2013 | Program Extraction from Nested Definitions. Kenji Miyamoto, Fredrik Nordvall Forsberg, Helmut Schwichtenberg |
| 2013 | Scalable LCF-Style Proof Translation. Cezary Kaliszyk, Alexander Krauss |
| 2013 | Shared-Memory Multiprocessing for Interactive Theorem Proving. Makarius Wenzel |
| 2013 | Square Root and Division Elimination in PVS. Pierre Neron |
| 2013 | Stateless Higher-Order Logic with Quantified Types. Evan Austin, Perry Alexander |
| 2013 | Steps towards Verified Implementations of HOL Light. Magnus O. Myreen, Scott Owens, Ramana Kumar |
| 2013 | Subformula Linking as an Interaction Method. Kaustuv Chaudhuri |
| 2013 | The Picard Algorithm for Ordinary Differential Equations in Coq. Evgeny Makarov, Bas Spitters |
| 2013 | Towards Certifying Network Calculus. Etienne Mabille, Marc Boyer, Loïc Fejoz, Stephan Merz |
| 2013 | Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. Johannes Hölzl, Fabian Immler, Brian Huffman |