Invited Talks.- A Formally Verified OS Kernel. Now What?.- Proof Assistants as Teaching Assistants: A View from the Trenches.- Proof Pearls.- A Certified Denotational Abstract Interpreter.- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure.- A New Foundation for Nominal Isabelle.- (Nominal) Unification by Recursive Descent with Triangular Substitutions.- A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks.- Regular Papers.- Extending Coq with Imperative Features and Its Application to SAT Verification.- A Tactic Language for Declarative Proofs.- Programming Language Techniques for Cryptographic Proofs.- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder.- Formal Proof of a Wave Equation Resolution Scheme: The Method Error.- An Efficient Coq Tactic for Deciding Kleene Algebras.- Fast LCF-Style Proof Reconstruction for Z3.- The Optimal Fixed Point Combinator.- Formal Study of Plane Delaunay Triangulation.- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison.- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.- Automated Machine-Checked Hybrid System Safety Proofs.- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study.- Case-Analysis for Rippling and Inductive Proof.- Importing HOL Light into Coq.- A Mechanized Translation from Higher-Order Logic to Set Theory.- The Isabelle Collections Framework.- Interactive Termination Proofs Using Termination Cores.- A Framework for Formal Verification of Compiler Optimizations.- On the Formalization of the Lebesgue Integration Theory in HOL.- From Total Store Order to Sequential Consistency: A Practical Reduction Theorem.- Equations: A Dependent Pattern-Matching Compiler.- A Mechanically Verified AIG-to-BDD Conversion Algorithm.- Inductive Consequences in the Calculus of Constructions.- Validating QBF Invalidity in HOL4.- Rough Diamonds.- Higher-Order Abstract Syntax in Isabelle/HOL.- Separation Logic Adapted for Proofs by Rewriting.- Developing the Algebraic Hierarchy with Type Classes in Coq.