TY  - BOOK
AU  - Blazy,Sandrine
AU  - Paulin-Mohring,Christine
AU  - Pichardie,David
TI  - Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings 
SN  - 9783642396342
PY  - 2013///
CY  - Berlin, Heidelberg
PB  - Springer Berlin Heidelberg
KW  - Computer science
KW  - Software engineering
KW  - Computer security
KW  - Algorithms
KW  - Computer logic
KW  - Mathematical logic
KW  - Artificial intelligence
N1  - 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
UR  - http://dx.doi.org/10.1007/978-3-642-39634-2
ER  -