000 04004nam a22006257a 4500
001 sulb-eb0023492
003 BD-SySUS
005 20160413122354.0
007 cr nn 008mamaa
008 131209s2013 gw | s |||| 0|eng d
020 _a9783319035451
_9978-3-319-03545-1
024 7 _a10.1007/978-3-319-03545-1
_2doi
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
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.
264 1 _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
347 _atext file
_bPDF
_2rda
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.
650 0 _aProgramming languages (Electronic computers).
650 0 _aComputer logic.
650 0 _aMathematical logic.
650 0 _aComputer science
_xMathematics.
650 0 _aArtificial intelligence.
650 1 4 _aComputer Science.
650 2 4 _aLogics and Meanings of Programs.
650 2 4 _aMathematical Logic and Formal Languages.
650 2 4 _aProgramming Languages, Compilers, Interpreters.
650 2 4 _aSymbolic and Algebraic Manipulation.
650 2 4 _aArtificial Intelligence (incl. Robotics).
650 2 4 _aComputer Science, general.
700 1 _aGonthier, Georges.
_eeditor.
700 1 _aNorrish, Michael.
_eeditor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9783319035444
830 0 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v8307
856 4 0 _uhttp://dx.doi.org/10.1007/978-3-319-03545-1
912 _aZDB-2-SCS
912 _aZDB-2-LNC
942 _2Dewey Decimal Classification
_ceBooks
999 _c45584
_d45584