Wow! eBook
Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13,2013, Proceedings
Author(s): Georges Gonthier (Editor), Michael Norrish
- Publisher: Springer
- Publication Date: November 27, 2013
- Language: English
- Print length: 324 pages
- ISBN-10: 3319035460
- ISBN-13: 9783319035468
Book Description
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.
