| 2012 | A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. Ruben Gamboa, John R. Cowles |
| 2012 | A Compact Proof of Decidability for Regular Expression Equivalence. Andrea Asperti |
| 2012 | A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). André Platzer |
| 2012 | A Language of Patterns for Subterm Selection. Georges Gonthier, Enrico Tassi |
| 2012 | A Refinement-Based Approach to Computational Algebra in Coq. Maxime Dénès, Anders Mörtberg, Vincent Siles |
| 2012 | Abella: A Tutorial. Andrew Gacek |
| 2012 | Abstract Interpretation of Annotated Commands. Tobias Nipkow |
| 2012 | Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. Peter Lammich, Thomas Tuerk |
| 2012 | Bag Equivalence via a Proof-Relevant Membership Relation. Nils Anders Danielsson |
| 2012 | Bridging the Gap: Automatic Verified Abstraction of C. David Greenaway, June Andronick, Gerwin Klein |
| 2012 | Certification of Nontermination Proofs. Christian Sternagel, René Thiemann |
| 2012 | Charge! - A Framework for Higher-Order Separation Logic in Coq. Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal |
| 2012 | Computer-Aided Cryptographic Proofs. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin |
| 2012 | Construction of Real Algebraic Numbers in Coq. Cyril Cohen |
| 2012 | Directions in ISA Specification. Anthony C. J. Fox |
| 2012 | Formalization of Shannon's Theorems in SSReflect-Coq. Reynald Affeldt, Manabu Hagiwara |
| 2012 | Functional Programs: Conversions between Deep and Shallow Embeddings. Magnus O. Myreen |
| 2012 | Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings Lennart Beringer, Amy P. Felty |
| 2012 | Mechanised Separation Algebra. Gerwin Klein, Rafal Kolanski, Andrew Boyton |
| 2012 | MetiTarski: Past and Future. Lawrence C. Paulson |
| 2012 | More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach |
| 2012 | Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. Fabian Immler, Johannes Hölzl |
| 2012 | Priority Inheritance Protocol Proved Correct. Xingyuan Zhang, Christian Urban, Chunhan Wu |
| 2012 | Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem. Lars Noschinski |
| 2012 | Standalone Tactics Using OpenTheory. Ramana Kumar, Joe Hurd |
| 2012 | Stop When You Are Almost-Full - Adventures in Constructive Termination. Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt |
| 2012 | Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. Marino Miculan, Marco Paviotti |
| 2012 | Towards Provably Robust Watermarking. David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring |
| 2012 | Using Locales to Define a Rely-Guarantee Temporal Logic. William Mansky, Elsa L. Gunter |
| 2012 | Verifying and Generating WP Transformers for Procedures on Complex Data. Patrick Michel, Arnd Poetzsch-Heffter |