LEADER 04498nam  22007695  450 
001 9910483078203321
005 20251226202949.0
010   $a3-319-03545-2
024 7 $a10.1007/978-3-319-03545-1
035   $a(CKB)3710000000078779
035   $a(DE-He213)978-3-319-03545-1
035   $a(SSID)ssj0001090369
035   $a(PQKBManifestationID)11631910
035   $a(PQKBTitleCode)TC0001090369
035   $a(PQKBWorkID)11135086
035   $a(PQKB)10728116
035   $a(MiAaPQ)EBC3096967
035   $a(PPN)176108114
035   $a(EXLCZ)993710000000078779
100   $a20131209d2013      u|         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt$2rdacontent
182   $cc$2rdamedia
183   $acr$2rdacarrier
200 10$aCertified Programs and Proofs $eThird International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13,2013, Proceedings /$fedited by Georges Gonthier, Michael Norrish
205   $a1st ed. 2013.
210  1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2013.
215   $a1 online resource (XII, 309 p. 44 illus.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v8307
300   $aBibliographic Level Mode of Issuance: Monograph
311 08$a3-319-03544-4 
327   $aInvited Lectures -- ?n(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot?s Gap Theorem -- Certified Kruskal?s Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework.
330   $aThis book constitutes the refereed proceedings of the Third International Conference on Certified Programs and Proofs, CPP 2013, colocated with APLAS 2013 held in Melbourne, Australia, in December 2013. The 18 revised regular papers presented together with 1 invited lecture were carefully reviewed and selected from 39 submissions. The papers are organized in topical sections on code verification, elegant proofs, proof libraries, certified transformations and security.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v8307
606   $aComputer science
606   $aMachine theory
606   $aCompilers (Computer programs)
606   $aComputer science$xMathematics
606   $aArtificial intelligence
606   $aComputer Science Logic and Foundations of Programming
606   $aFormal Languages and Automata Theory
606   $aCompilers and Interpreters
606   $aSymbolic and Algebraic Manipulation
606   $aArtificial Intelligence
606   $aComputer Science
615  0$aComputer science.
615  0$aMachine theory.
615  0$aCompilers (Computer programs).
615  0$aComputer science$xMathematics.
615  0$aArtificial intelligence.
615 14$aComputer Science Logic and Foundations of Programming.
615 24$aFormal Languages and Automata Theory.
615 24$aCompilers and Interpreters.
615 24$aSymbolic and Algebraic Manipulation.
615 24$aArtificial Intelligence.
615 24$aComputer Science.
676   $a004.0151
702   $aGonthier$b Georges$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aNorrish$b Michael$4edt$4http://id.loc.gov/vocabulary/relators/edt
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910483078203321
996   $aCertified Programs and Proofs$92557693
997   $aUNINA