| 2011 | A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). Chunhan Wu, Xingyuan Zhang, Christian Urban |
| 2011 | A Formalization of Polytime Functions. Sylvain Heraud, David Nowak |
| 2011 | A Verified Runtime for a Verified Theorem Prover. Magnus O. Myreen, Jared Davis |
| 2011 | Advances in the Formalization of the Odd Order Theorem. Georges Gonthier |
| 2011 | Animating the Formalised Semantics of a Java-Like Language. Andreas Lochbihler, Lukas Bulwahn |
| 2011 | Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina |
| 2011 | Automatic Differentiation in ACL2. Peter Reid, Ruben Gamboa |
| 2011 | Challenges in Verifying Communication Fabrics. Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov |
| 2011 | Composable Discovery Engines for Interactive Theorem Proving. Phil Scott, Jacques D. Fleuriot |
| 2011 | Formalization of Entropy Measures in HOL. Tarek Mhamdi, Osman Hasan, Sofiène Tahar |
| 2011 | Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers. Matej Urbas, Mateja Jamnik |
| 2011 | Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk |
| 2011 | LCF-Style Bit-Blasting in HOL4. Anthony C. J. Fox |
| 2011 | Lem: A Lightweight Tool for Heavyweight Semantics. Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell |
| 2011 | Logical Formalisation and Analysis of the Mifare Classic Card in PVS. Bart Jacobs, Ronny Wichers Schreur |
| 2011 | Mechanised Computability Theory. Michael Norrish |
| 2011 | On the Generation of Positivstellensatz Witnesses in Degenerate Cases. David Monniaux, Pierre Corbineau |
| 2011 | Point-Free, Set-Free Concrete Linear Algebra. Georges Gonthier |
| 2011 | Proving Valid Quantified Boolean Formulas in HOL Light. Ondrej Kuncar |
| 2011 | Relational Decomposition. Lennart Beringer |
| 2011 | Structural Analysis of Narratives with the Coq Proof Assistant. Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza |
| 2011 | Termination of Isabelle Functions via Termination of Rewriting. Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl |
| 2011 | Three Chapters of Measure Theory in Isabelle/HOL. Johannes Hölzl, Armin Heller |
| 2011 | Towards Robustness Analysis Using PVS. Renaud Clavel, Laurence Pierre, Régis Leveugle |
| 2011 | Towards Verification of Product Lines. Don S. Batory |
| 2011 | Validating QBF Validity in HOL4. Ramana Kumar, Tjark Weber |
| 2011 | Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. Tobias Nipkow |
| 2011 | Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. Peter Gammie |
| 2011 | Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal |
| 2011 | seL4 Enforces Integrity. Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein |