| 2012 | Proof Pearl: Abella Formalization of λ-Calculus Cube Property. | Beniamino Accattoli |
| 2011 | Univalent Semantics of Constructive Type Theories. | Vladimir Voevodsky |
| 2011 | Automated Certification of Implicit Induction Proofs. | Sorin Stratulat, Vincent Demange |
| 2011 | First Steps towards the Certification of an ARM Simulator Using Compcert. | Xiaomu Shi, Jean-Franois Monin, Frdric Tuong, Frdric Blanqui |
| 2011 | Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars. | Tom Ridge |
| 2011 | Proof-Carrying Code in a Session-Typed Process Calculus. | Frank Pfenning, Lus Caires, Bernardo Toninho |
| 2011 | Algebra, Logic, Locality, Concurrency. | Peter W. O'Hearn |
| 2011 | Hardware-Dependent Proofs of Numerical Programs. | Thi Minh Tuyen Nguyen, Claude March |
| 2011 | A Proposal for Broad Spectrum Proof Certificates. | Dale Miller |
| 2011 | Verification of Scalable Synchronous Queue. | Jinjiang Lei, Zongyan Qiu |
| 2011 | Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. | Jieung Kim, Sukyoung Ryu |
| 2011 | Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. | Cezary Kaliszyk, Henk Barendregt |
| 2011 | The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math". | Wolfram Kahl |
| 2011 | Proof Pearl: The Marriage Theorem. | Dongchen Jiang, Tobias Nipkow |
| 2011 | Teaching Experience: Logic and Formal Methods with Coq. | Martin Henz, Aquinas Hobor |
| 2011 | Formalization of Wu's Simple Method in Coq. | Jean-David Gnevaux, Julien Narboux, Pascal Schreck |
| 2011 | Constructive Formalization of Hybrid Logic with Eventualities. | Christian Doczkal, Gert Smolka |
| 2011 | Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. | Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech |
| 2011 | A Decision Procedure for Regular Expression Equivalence in Type Theory. | Thierry Coquand, Vincent Siles |
| 2011 | Mechanizing the Metatheory of mini-XQuery. | James Cheney, Christian Urban |
| 2011 | Tactics for Reasoning Modulo AC in Coq. | Thomas Braibant, Damien Pous |
| 2011 | Coquet: A Coq Library for Verifying Hardware. | Thomas Braibant |
| 2011 | Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. | Sascha Bhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber |
| 2011 | Full Reduction at Full Throttle. | Mathieu Boespflug, Maxime Dns, Benjamin Grgoire |
| 2011 | Engineering Theories with Z3. | Nikolaj S. Bjrner |