Interactive Theorem Proving

MetiTarski: Past and Future.- Computer-Aided Cryptographic Proofs.- A Differential Operator Approach to Equational Differential Invariants.- Abella: A Tutorial.- A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers.- Construction of Real Algebraic Numbers in Coq.- A Refinement-Based Approach to Computational Algebra in Coq.- Bridging the Gap: Automatic Verified Abstraction of C.- Abstract Interpretation of Annotated Commands.- Verifying and Generating WP Transformers for Procedures on Complex Data.- Bag Equivalence via a Proof-Relevant Membership Relation.- Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm.- Synthesis of Distributed Mobile Programs Using Monadic Types in Coq.- Towards Provably Robust Watermarking.- Priority Inheritance Protocol Proved Correct.- Formalization of Shannon's Theorems in SSReflect-Coq.- Stop When You Are Almost-Full: Adventures in Constructive Termination.- Certification of Nontermination Proofs.- A Compact Proof of Decidability for Regular Expression Equivalence.- Using Locales to Define a Rely-Guarantee Temporal Logic.- Charge! - A Framework for Higher-Order Separation Logic in Coq.- Mechanised Separation Algebra.- Directions in ISA Specification.- More SPASS with Isabelle: Superposition with Hard Sorts and Configurable Simplification.- A Language of Patterns for Subterm Selection.- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL.- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem.- Standalone Tactics Using OpenTheory.- Functional Programs: Conversions between Deep and Shallow Embeddings.