TY  - BOOK
AU  - Gonthier,Georges
AU  - Norrish,Michael
TI  - Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings 
SN  - 9783319035451
PY  - 2013///
CY  - Cham
PB  - Springer International Publishing
KW  - Computer science
KW  - Programming languages (Electronic computers)
KW  - Computer logic
KW  - Mathematical logic
KW  - Mathematics
KW  - Artificial intelligence
N1  - 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
UR  - http://dx.doi.org/10.1007/978-3-319-03545-1
ER  -