Interactive Theorem Proving [electronic resource] : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings / edited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie.

Invited Talks -- Applying Formal Methods in the Large -- Automating Theorem Proving with SMT -- Certifying Voting Protocols -- Invited Tutorials.-Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities -- Canonical Structures for the Working Coq User -- Regular Papers -- MaSh: Machine Learning for Sledgehammer -- Scalable LCF-Style Proof Translation -- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation -- Automatic Data Refinement -- Data Refinement in Isabelle/HOL -- Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable -- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1 -- Mechanising Turing Machines and Computability Theory in Isabelle/HOL.-A Machine-Checked Proof of the Odd Order Theorem -- Kleene Algebra with Tests and Coq Tools for while Programs.-Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL -- Pragmatic Quotient Types in Coq -- Mechanical Verification of SAT Refutations with Extended Resolution -- Formalizing Bounded Increase -- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types -- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL -- Formal Reasoning about Classified Markov Chains in HOL -- Practical Probability: Applying pGCL to Lattice Scheduling -- Adjustable References -- Handcrafted Inversions Made Operational on Operational Semantics -- Circular Coinduction in Coq Using Bisimulation-Up-To Techniques -- Program Extraction from Nested Definitions -- Subformula Linking as an Interaction Method -- Automatically Generated Infrastructure for De Bruijn Syntaxes -- Shared-Memory Multiprocessing for Interactive Theorem Proving -- A Parallelized Theorem Prover for a Logic with Parallel Execution -- Rough Diamonds -- Communicating Formal Proofs: The Case of Flyspeck -- Square Root and Division Elimination in PVS -- The Picard Algorithm for Ordinary Differential Equations in Coq -- Stateless Higher-Order Logic with Quantified Types -- Implementing Hash-Consed Structures in Coq -- Towards Certifying Network Calculus -- Steps towards Verified Implementations of HOL Light.