Certified Programs and Proofs  Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings /  [electronic resource] : 
edited by Georges Gonthier, Michael Norrish. 
 - Cham :  Springer International Publishing,  2013. 
 - 1 online resource (XII, 309 p. 44 ill.) 
 - Lecture Notes in Computer Science,  8307  0302-9743 ; .
<br/><br/>Invited 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. 
<br/><br/><label>ISBN: </label>9783319035451 
<br/><br/><label>Subjects--Topical Terms: </label><br/>Computer science.<br/>Programming languages (Electronic computers).<br/>Computer logic.<br/>Mathematical logic.<br/>Computer science--Mathematics.<br/>Artificial intelligence.