000 04030nam a22006015i 4500
001 vtls000484206
003 RU-ToGU
005 20210922065426.0
007 cr nn 008mamaa
008 140715s2013 gw | s |||| 0|eng d
020 _a9783319035451
_9978-3-319-03545-1
024 7 _a10.1007/978-3-319-03545-1
_2doi
035 _ato000484206
040 _aSpringer
_cSpringer
_dRU-ToGU
050 4 _aQA76.9.L63
050 4 _aQA76.5913
050 4 _aQA76.63
072 7 _aUM
_2bicssc
072 7 _aUYF
_2bicssc
072 7 _aCOM051000
_2bisacsh
072 7 _aCOM036000
_2bisacsh
082 0 4 _a005.1015113
_223
100 1 _aGonthier, Georges.
_eeditor.
_9412450
245 1 0 _aCertified Programs and Proofs
_h[electronic resource] :
_bThird International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings /
_cedited by Georges Gonthier, Michael Norrish.
260 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2013.
300 _aXII, 309 p. 44 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
490 1 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v8307
505 0 _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.
520 _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.
650 0 _aComputer Science.
_9155490
650 0 _aLogic design.
_9306256
650 0 _aAlgebra
_xData processing.
_9304851
650 0 _aArtificial intelligence.
_9274099
650 1 4 _aComputer Science.
_9155490
650 2 4 _aLogics and Meanings of Programs.
_9306257
650 2 4 _aMathematical Logic and Formal Languages.
_9303363
650 2 4 _aProgramming Languages, Compilers, Interpreters.
_9303287
650 2 4 _aSymbolic and Algebraic Manipulation.
_9566359
650 2 4 _aArtificial Intelligence (incl. Robotics).
_9274102
650 2 4 _aComputer Science, general.
_9155491
700 1 _aNorrish, Michael.
_eeditor.
_9412451
710 2 _aSpringerLink (Online service)
_9143950
773 0 _tSpringer eBooks
830 0 _aLecture Notes in Computer Science,
_9279505
856 4 0 _uhttp://dx.doi.org/10.1007/978-3-319-03545-1
912 _aZDB-2-SCS
912 _aZDB-2-LNC
999 _c355615