| 2010 | (Nominal) Unification by Recursive Descent with Triangular Substitutions. Ramana Kumar, Michael Norrish |
| 2010 | A Certified Denotational Abstract Interpreter. David Cachera, David Pichardie |
| 2010 | A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. Freek Verbeek, Julien Schmaltz |
| 2010 | A Formally Verified OS Kernel. Now What? Gerwin Klein |
| 2010 | A Framework for Formal Verification of Compiler Optimizations. William Mansky, Elsa L. Gunter |
| 2010 | A Mechanically Verified AIG-to-BDD Conversion Algorithm. Sol Swords, Warren A. Hunt Jr. |
| 2010 | A Mechanized Translation from Higher-Order Logic to Set Theory. Alexander Krauss, Andreas Schropp |
| 2010 | A New Foundation for Nominal Isabelle. Brian Huffman, Christian Urban |
| 2010 | A Tactic Language for Declarative Proofs. Serge Autexier, Dominik Dietrich |
| 2010 | A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. Anthony C. J. Fox, Magnus O. Myreen |
| 2010 | An Efficient Coq Tactic for Deciding Kleene Algebras. Thomas Braibant, Damien Pous |
| 2010 | Automated Machine-Checked Hybrid System Safety Proofs. Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen |
| 2010 | Case-Analysis for Rippling and Inductive Proof. Moa Johansson, Lucas Dixon, Alan Bundy |
| 2010 | Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. Joe Hendrix, Deepak Kapur, José Meseguer |
| 2010 | Developing the Algebraic Hierarchy with Type Classes in Coq. Bas Spitters, Eelis van der Weegen |
| 2010 | Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau |
| 2010 | Extending Coq with Imperative Features and Its Application to SAT Verification. Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry |
| 2010 | Fast LCF-Style Proof Reconstruction for Z3. Sascha Böhme, Tjark Weber |
| 2010 | Formal Proof of a Wave Equation Resolution Scheme: The Method Error. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis |
| 2010 | Formal Study of Plane Delaunay Triangulation. Jean-François Dufourd, Yves Bertot |
| 2010 | From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. Ernie Cohen, Bert Schirmer |
| 2010 | Higher-Order Abstract Syntax in Isabelle/HOL. Douglas J. Howe |
| 2010 | Importing HOL Light into Coq. Chantal Keller, Benjamin Werner |
| 2010 | Inductive Consequences in the Calculus of Constructions. Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
| 2010 | Interactive Termination Proofs Using Termination Cores. Panagiotis Manolios, Daron Vroon |
| 2010 | Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings Matt Kaufmann, Lawrence C. Paulson |
| 2010 | Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. Jasmin Christian Blanchette, Tobias Nipkow |
| 2010 | On the Formalization of the Lebesgue Integration Theory in HOL. Tarek Mhamdi, Osman Hasan, Sofiène Tahar |
| 2010 | Programming Language Techniques for Cryptographic Proofs. Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin |
| 2010 | Proof Assistants as Teaching Assistants: A View from the Trenches. Benjamin C. Pierce |
| 2010 | Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. Amy P. Felty, Brigitte Pientka |
| 2010 | Separation Logic Adapted for Proofs by Rewriting. Magnus O. Myreen |
| 2010 | The Isabelle Collections Framework. Peter Lammich, Andreas Lochbihler |
| 2010 | The Optimal Fixed Point Combinator. Arthur Charguéraud |
| 2010 | Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. John R. Cowles, Ruben Gamboa |
| 2010 | Validating QBF Invalidity in HOL4. Tjark Weber |