LEADER 04578nam  22008295  450 
001 9910483598903321
005 20230329141710.0
010   $a3-319-22102-7
024 7 $a10.1007/978-3-319-22102-1
035   $a(CKB)3890000000001331
035   $a(SSID)ssj0001558566
035   $a(PQKBManifestationID)16183032
035   $a(PQKBTitleCode)TC0001558566
035   $a(PQKBWorkID)14819122
035   $a(PQKB)11787708
035   $a(DE-He213)978-3-319-22102-1
035   $a(MiAaPQ)EBC6288126
035   $a(MiAaPQ)EBC5579423
035   $a(Au-PeEL)EBL5579423
035   $a(OCoLC)919251295
035   $a(PPN)188460292
035   $a(EXLCZ)993890000000001331
100   $a20150818d2015      u|         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aInteractive Theorem Proving $e6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings /$fedited by Christian Urban, Xingyuan Zhang
205   $a1st ed. 2015.
210  1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2015.
215   $a1 online resource (XI, 469 p. 63 illus.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v9236
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-319-22101-9 
327   $aVerified, Practical Upper Bounds for State Space Diameters -- Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory -- ROSCoq: Robots powered by Constructive Reals -- Asynchronous processing of Coq documents: from the kernel up to the user interface -- A Concrete Memory Model for CompCert -- Validating Dominator Trees for a Fast, Verified Dominance Test -- Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra -- Mechanisation of AKS Algorithm -- Machine-Checked Verification of the Correctness and Amortized -- Improved Tool Support for Machine-Code Decompilation in HOL4 -- A Formalized Hierarchy of Probabilistic System Types -- Learning To Parse on Aligned Corpora -- A Consistent Foundation for Isabelle/HOL -- Foundational Property-Based Testing -- A First-Order Functional Intermediate Language for Verified Compilers -- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions -- ModuRes: a Coq Library for Modular Reasoning about Concurrent -- Higher-Order Imperative Programming Languages -- Transfinite Constructions in Classical Type Theory -- A Mechanized Theory of regular trees in dependent type theory -- Deriving Comparators and Show-Functions in Isabelle/HOL -- Formalizing Knot Theory in Isabelle/HOL -- Pattern Matches in HOL: A New Representation and Improved Code Generation.
330   $aThis book constitutes the proceedings of the 6th International Conference on Interactive Theorem Proving, ITP 2015, held in Nanjing, China, in August 2015. The 27 papers presented in this volume were carefully reviewed and selected from 54 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v9236
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   $aUrban$b Christian$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aZhang$b Xingyuan$4edt$4http://id.loc.gov/vocabulary/relators/edt
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910483598903321
996   $aInteractive Theorem Proving$92010767
997   $aUNINA