Skip to main content
SpringerLink
Log in
Book cover
  • Conference proceedings
  • © 2013

Certified Programs and Proofs

Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13,2013, Proceedings

Editors:

  1. Georges Gonthier

    1. Microsoft Research Cambridge, Cambridge, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Michael Norrish

    1. Canberra Research Lab., NICTA, Canberra, Australia

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Up-to-date results Proceedings of the Third International Conference on Certified Programs and Proofs, CPP 2013

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 8307)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Conference series link(s): CPP: International Conference on Certified Programs and Proofs

Conference proceedings info: CPP 2013.

Sections

Buy it now

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (19 papers)

  1. Front Matter

    PDF

  2. Invited Lectures

    1. π n (S n) in Homotopy Type Theory

      • Daniel R. Licata, Guillaume Brunerie
      Pages 1-16

  3. Session 1: Code Verification

    1. Mostly Sound Type System Improves a Foundational Program Verifier

      • Josiah Dodds, Andrew W. Appel
      Pages 17-32

    3. Aliasing Restrictions of C11 Formalized in Coq

      • Robbert Krebbers
      Pages 50-65

  4. Session 2: Elegant Proofs

    1. Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code

      • Magnus O. Myreen, Gregorio Curello
      Pages 66-81

    2. A Constructive Theory of Regular Languages in Coq

      • Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka
      Pages 82-97

    3. Certified Parsing of Regular Languages

      • Denis Firsov, Tarmo Uustalu
      Pages 98-113

  5. Session 3: Proof Libraries

    1. Nonfree Datatypes in Isabelle/HOL

      • Andreas Schropp, Andrei Popescu
      Pages 114-130

    2. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

      • Brian Huffman, Ondřej Kunčar
      Pages 131-146

    3. Refinements for Free!

      • Cyril Cohen, Maxime Dénès, Anders Mörtberg
      Pages 147-162

  6. Session 4: Mathematics

    2. Certified Kruskal’s Tree Theorem

      • Christian Sternagel
      Pages 178-193

    3. Extracting Proofs from Tabled Proof Search

      • Dale Miller, Alwen Tiu
      Pages 194-210

  7. Session 5: Certified Transformations

    1. Formalizing the SAFECode Type System

      • Daniel Huang, Greg Morrisett
      Pages 211-226

    2. Certifiably Sound Parallelizing Transformations

      • Christian J. Bell
      Pages 227-242

    3. Programming Type-Safe Transformations Using Higher-Order Abstract Syntax

      • Olivier Savary-Belanger, Stefan Monnier, Brigitte Pientka
      Pages 243-258

  8. Session 6: Security

    1. Formalizing Probabilistic Noninterference

      • Andrei Popescu, Johannes Hölzl, Tobias Nipkow
      Pages 259-275

    2. Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties

      • Narges Khakpour, Oliver Schwarz, Mads Dam
      Pages 276-291

    3. A Formal Model and Correctness Proof for an Access Control Policy Framework

      • Chunhan Wu, Xingyuan Zhang, Christian Urban
      Pages 292-307
Back to top

Other Volumes

  1. Certified Programs and Proofs

Back to top

About this book

This 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.
Back to top

Keywords

Back to top

Editors and Affiliations

  • Microsoft Research Cambridge, Cambridge, UK

    Georges Gonthier

  • Canberra Research Lab., NICTA, Canberra, Australia

    Michael Norrish

Back to top

Bibliographic Information

Back to top

Publish with us

Policies and ethics

Back to top
Access via your institution

Buy it now

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Search

Navigation