Skip to main content
SpringerLink
Log in

Certified Programs and Proofs

First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011, Proceedings

  • Conference proceedings
  • © 2011

Overview

Editors:
  1. Jean-Pierre Jouannaud

    1. Tsinghua University, Beijing, China

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Zhong Shao

    1. Department of Computer Science, Yale University, New Haven, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Fast track conference proceedings
  • Unique visibility
  • State of the art research

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

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

Included in the following conference series:

Conference proceedings info: CPP 2011.

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 (28 papers)

  1. Front Matter

    Download chapter PDF

  2. APLAS/CPP Invited Talks

    1. Engineering Theories with Z3

      • Nikolaj Bjørner
      Pages 1-2

    2. Algebra, Logic, Locality, Concurrency

      • Peter W. O’Hearn
      Pages 3-4

  3. Session 1: Logic and Types

    1. Constructive Formalization of Hybrid Logic with Eventualities

      • Christian Doczkal, Gert Smolka
      Pages 5-20

    2. Proof-Carrying Code in a Session-Typed Process Calculus

      • Frank Pfenning, Luis Caires, Bernardo Toninho
      Pages 21-36

  4. Session 2: Certificates

    1. Automated Certification of Implicit Induction Proofs

      • Sorin Stratulat, Vincent Demange
      Pages 37-53

    2. A Proposal for Broad Spectrum Proof Certificates

      • Dale Miller
      Pages 54-69

  5. Session 3: Invited Talk

    1. Univalent Semantics of Constructive Type Theories

      • Vladimir Voevodsky
      Pages 70-70

  6. Session 4: Formalization

    1. Formalization of Wu’s Simple Method in Coq

      • Jean-David Génevaux, Julien Narboux, Pascal Schreck
      Pages 71-86

    2. Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem

      • Cezary Kaliszyk, Henk Barendregt
      Pages 87-102

    3. Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars

      • Tom Ridge
      Pages 103-118

    4. A Decision Procedure for Regular Expression Equivalence in Type Theory

      • Thierry Coquand, Vincent Siles
      Pages 119-134

  7. Session 5: Proof Assistants

    1. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

      • Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner
      Pages 135-150

    2. Modular SMT Proofs for Fast Reflexive Checking Inside Coq

      • Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
      Pages 151-166

    3. Tactics for Reasoning Modulo AC in Coq

      • Thomas Braibant, Damien Pous
      Pages 167-182

    4. Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL

      • Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber
      Pages 183-198

  9. Session 7: Invited Talk

    1. VeriSmall: Verified Smallfoot Shape Analysis

      • Andrew W. Appel
      Pages 231-246

  10. Session 8: Programming Languages

    1. Verification of Scalable Synchronous Queue

      • Jinjiang Lei, Zongyan Qiu
      Pages 247-263
Back to top

Other volumes

  1. Certified Programs and Proofs

Keywords

About this book

This book constitutes the referred proceedings of the First International Conference on Certified Programs and Proofs, CPP 2011, held in Kenting, Taiwan, in December 2011.
The 24 revised regular papers presented together with 4 invited talks were carefully reviewed and selected from 49 submissions. They are organized in topical sections on logic and types, certificates, formalization, proof assistants, teaching, programming languages, hardware certification, miscellaneous, and proof perls.

Editors and Affiliations

  • Tsinghua University, Beijing, China

    Jean-Pierre Jouannaud

  • Department of Computer Science, Yale University, New Haven, USA

    Zhong Shao

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation