Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Certified Programs and Proofs

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

  • Conference proceedings
  • © 2013

Overview

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)

Included in the following conference series:

Conference proceedings info: CPP 2013.

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

Access this book

Log in via an institution
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

Licence this eBook for your library

Institutional subscriptions

Table of contents (19 papers)

  1. Front Matter

    Download chapter 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

    2. Computational Verification of Network Programs in Coq

      • Gordon Stewart
      Pages 33-49

    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

    1. A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem

      • Andrea Asperti
      Pages 163-177

    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

Keywords

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.

Editors and Affiliations

  • Microsoft Research Cambridge, Cambridge, UK

    Georges Gonthier

  • Canberra Research Lab., NICTA, Canberra, Australia

    Michael Norrish

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation