| 2011 | A Decision Procedure for Regular Expression Equivalence in Type Theory. Thierry Coquand, Vincent Siles |
| 2011 | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner |
| 2011 | A Proposal for Broad Spectrum Proof Certificates. Dale Miller |
| 2011 | Algebra, Logic, Locality, Concurrency. Peter W. O'Hearn |
| 2011 | Automated Certification of Implicit Induction Proofs. Sorin Stratulat, Vincent Demange |
| 2011 | Automatically Verifying Typing Constraints for a Data Processing Language. Michael Backes, Catalin Hritcu, Thorsten Tarrach |
| 2011 | Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings Jean-Pierre Jouannaud, Zhong Shao |
| 2011 | Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech |
| 2011 | Constructive Formalization of Hybrid Logic with Eventualities. Christian Doczkal, Gert Smolka |
| 2011 | Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. Jieung Kim, Sukyoung Ryu |
| 2011 | Coquet: A Coq Library for Verifying Hardware. Thomas Braibant |
| 2011 | Engineering Theories with Z3. Nikolaj S. Bjørner |
| 2011 | First Steps towards the Certification of an ARM Simulator Using Compcert. Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui |
| 2011 | Formalization of Wu's Simple Method in Coq. Jean-David Génevaux, Julien Narboux, Pascal Schreck |
| 2011 | Full Reduction at Full Throttle. Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire |
| 2011 | Hardware-Dependent Proofs of Numerical Programs. Thi Minh Tuyen Nguyen, Claude Marché |
| 2011 | Mechanizing the Metatheory of mini-XQuery. James Cheney, Christian Urban |
| 2011 | Modular SMT Proofs for Fast Reflexive Checking Inside Coq. Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie |
| 2011 | Proof Pearl: The Marriage Theorem. Dongchen Jiang, Tobias Nipkow |
| 2011 | Proof-Carrying Code in a Session-Typed Process Calculus. Frank Pfenning, Luís Caires, Bernardo Toninho |
| 2011 | Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. Cezary Kaliszyk, Henk Barendregt |
| 2011 | Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber |
| 2011 | Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars. Tom Ridge |
| 2011 | Tactics for Reasoning Modulo AC in Coq. Thomas Braibant, Damien Pous |
| 2011 | Teaching Experience: Logic and Formal Methods with Coq. Martin Henz, Aquinas Hobor |
| 2011 | The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math". Wolfram Kahl |
| 2011 | Univalent Semantics of Constructive Type Theories. Vladimir Voevodsky |
| 2011 | VeriSmall: Verified Smallfoot Shape Analysis. Andrew W. Appel |
| 2011 | Verification of Scalable Synchronous Queue. Jinjiang Lei, Zongyan Qiu |