| 2010 | Djinn, Monotonic. | Conor McBride |
| 2010 | A Framework for Formal Verification of Compiler Optimizations. | William Mansky, Elsa L. Gunter |
| 2010 | Interactive Termination Proofs Using Termination Cores. | Panagiotis Manolios, Daron Vroon |
| 2010 | Rewriting and Well-Definedness within a Proof System. | Issam Maamria, Michael J. Butler |
| 2010 | The Isabelle Collections Framework. | Peter Lammich, Andreas Lochbihler |
| 2010 | (Nominal) Unification by Recursive Descent with Triangular Substitutions. | Ramana Kumar, Michael Norrish |
| 2010 | A Mechanized Translation from Higher-Order Logic to Set Theory. | Alexander Krauss, Andreas Schropp |
| 2010 | Recursive Definitions of Monadic Functions. | Alexander Krauss |
| 2010 | A Formally Verified OS Kernel. Now What? | Gerwin Klein |
| 2010 | Importing HOL Light into Coq. | Chantal Keller, Benjamin Werner |
| 2010 | Case-Analysis for Rippling and Inductive Proof. | Moa Johansson, Lucas Dixon, Alan Bundy |
| 2010 | A New Foundation for Nominal Isabelle. | Brian Huffman, Christian Urban |
| 2010 | Higher-Order Abstract Syntax in Isabelle/HOL. | Douglas J. Howe |
| 2010 | Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. | Joe Hendrix, Deepak Kapur, Jos Meseguer |
| 2010 | Automated Machine-Checked Hybrid System Safety Proofs. | Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen |
| 2010 | A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. | Anthony C. J. Fox, Magnus O. Myreen |
| 2010 | Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. | Amy P. Felty, Brigitte Pientka |
| 2010 | Formal Study of Plane Delaunay Triangulation. | Jean-Franois Dufourd, Yves Bertot |
| 2010 | Beating the Productivity Checker Using Embedded Languages. | Nils Anders Danielsson |
| 2010 | Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. | John R. Cowles, Ruben Gamboa |
| 2010 | From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. | Ernie Cohen, Bert Schirmer |
| 2010 | General Recursion and Formal Topology. | Claudio Sacerdoti Coen, Silvio Valentini |
| 2010 | The Optimal Fixed Point Combinator. | Arthur Charguraud |
| 2010 | A Certified Denotational Abstract Interpreter. | David Cachera, David Pichardie |
| 2010 | An Efficient Coq Tactic for Deciding Kleene Algebras. | Thomas Braibant, Damien Pous |