Certified Programs and Proofs

1. Front Matter

   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

8. Session 6: Teaching

   1. Teaching Experience: Logic and Formal Methods with Coq

      • Martin Henz, Aquinas Hobor

      Pages 199-215

   2. The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”

      • Wolfram Kahl

      Pages 216-230

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

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.

• Isabelle/HOL
• decision procedures
• formal verification
• provable cryptography
• typechecking

• Tsinghua University, Beijing, China

  Jean-Pierre Jouannaud

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

  Zhong Shao

Policies and ethics