LEADER 05558nam 22008175 450 001 9910483676803321 005 20230329141200.0 010 $a3-642-39634-8 024 7 $a10.1007/978-3-642-39634-2 035 $a(CKB)3710000000002639 035 $a(SSID)ssj0000962843 035 $a(PQKBManifestationID)11573006 035 $a(PQKBTitleCode)TC0000962843 035 $a(PQKBWorkID)10976365 035 $a(PQKB)10061076 035 $a(DE-He213)978-3-642-39634-2 035 $a(MiAaPQ)EBC3101196 035 $a(PPN)172428416 035 $a(EXLCZ)993710000000002639 100 $a20130722d2013 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aInteractive Theorem Proving $e4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings /$fedited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie 205 $a1st ed. 2013. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2013. 215 $a1 online resource (XII, 498 p. 73 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7998 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-39633-X 320 $aIncludes bibliographical references and index. 327 $aInvited 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. 330 $aThis book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7998 606 $aMachine theory 606 $aArtificial intelligence 606 $aComputer science 606 $aSoftware engineering 606 $aData protection 606 $aAlgorithms 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aData and Information Security 606 $aAlgorithms 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aData protection. 615 0$aAlgorithms. 615 14$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aData and Information Security. 615 24$aAlgorithms. 676 $a004.015113 702 $aBlazy$b Sandrine$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aPaulin-Mohring$b Christine$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aPichardie$b David$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483676803321 996 $aInteractive Theorem Proving$92010767 997 $aUNINA