Advertisement

Certified Programs and Proofs

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

  • Jean-Pierre Jouannaud
  • Zhong Shao

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

Table of contents

  1. Front Matter
  2. APLAS/CPP Invited Talks

    1. Nikolaj Bjørner
      Pages 1-2
    2. Peter W. O’Hearn
      Pages 3-4
  3. Session 1: Logic and Types

    1. Christian Doczkal, Gert Smolka
      Pages 5-20
    2. Frank Pfenning, Luis Caires, Bernardo Toninho
      Pages 21-36
  4. Session 2: Certificates

    1. Sorin Stratulat, Vincent Demange
      Pages 37-53
  5. Session 3: Invited Talk

  6. Session 4: Formalization

  7. Session 5: Proof Assistants

    1. Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner
      Pages 135-150
    2. Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
      Pages 151-166
    3. Thomas Braibant, Damien Pous
      Pages 167-182
    4. Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber
      Pages 183-198
  8. Session 6: Teaching

  9. Session 7: Invited Talk

    1. Andrew W. Appel
      Pages 231-246
  10. Session 8: Programming Languages

    1. Jinjiang Lei, Zongyan Qiu
      Pages 247-263
    2. James Cheney, Christian Urban
      Pages 280-295
    3. Michael Backes, Cătălin Hriţcu, Thorsten Tarrach
      Pages 296-313
  11. Session 9: Hardware Certification

    1. Thi Minh Tuyen Nguyen, Claude Marché
      Pages 314-329
    2. Thomas Braibant
      Pages 330-345
    3. Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui
      Pages 346-361
  12. Session 10: Miscellaneous

    1. Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire
      Pages 362-377
  13. Session 11: Proof Pearls

    1. Dongchen Jiang, Tobias Nipkow
      Pages 394-399
  14. Back Matter

About these proceedings

Introduction

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.

Keywords

Isabelle/HOL decision procedures formal verification provable cryptography typechecking

Editors and affiliations

  • Jean-Pierre Jouannaud
    • 1
  • Zhong Shao
    • 2
  1. 1.Tsinghua UniversityBeijingChina
  2. 2.Department of Computer ScienceYale UniversityNew HavenUSA

Bibliographic information

  • DOI https://doi.org/10.1007/978-3-642-25379-9
  • Copyright Information Springer-Verlag GmbH Berlin Heidelberg 2011
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Computer Science
  • Print ISBN 978-3-642-25378-2
  • Online ISBN 978-3-642-25379-9
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
Electronics
IT & Software
Aerospace