Interactive Theorem Proving

1. Front Matter

   PDF

2. Invited Talks

   1. MetiTarski: Past and Future

      • Lawrence C. Paulson

      Pages 1-10

   2. Computer-Aided Cryptographic Proofs

      • Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin

      Pages 11-27

   3. A Differential Operator Approach to Equational Differential Invariants

      • André Platzer

      Pages 28-48

3. Invited Tutorial

   1. Abella: A Tutorial

      • Andrew Gacek

      Pages 49-50

4. Formalization of Mathematics I

   1. A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers

      • Ruben Gamboa, John Cowles

      Pages 51-66

   2. Construction of Real Algebraic Numbers in Coq

      • Cyril Cohen

      Pages 67-82

   3. A Refinement-Based Approach to Computational Algebra in Coq

      • Maxime Dénès, Anders Mörtberg, Vincent Siles

      Pages 83-98

5. Program Abstraction and Logics

   1. Bridging the Gap: Automatic Verified Abstraction of C

      • David Greenaway, June Andronick, Gerwin Klein

      Pages 99-115

   2. Abstract Interpretation of Annotated Commands

      • Tobias Nipkow

      Pages 116-132

   3. Verifying and Generating WP Transformers for Procedures on Complex Data

      • Patrick Michel, Arnd Poetzsch-Heffter

      Pages 133-148

6. Data Structures and Synthesis

   1. Bag Equivalence via a Proof-Relevant Membership Relation

      • Nils Anders Danielsson

      Pages 149-165

   2. Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm

      • Peter Lammich, Thomas Tuerk

      Pages 166-182

   3. Synthesis of Distributed Mobile Programs Using Monadic Types in Coq

      • Marino Miculan, Marco Paviotti

      Pages 183-200

7. Security

   1. Towards Provably Robust Watermarking

      • David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring

      Pages 201-216

   2. Priority Inheritance Protocol Proved Correct

      • Xingyuan Zhang, Christian Urban, Chunhan Wu

      Pages 217-232

   3. Formalization of Shannon’s Theorems in SSReflect-Coq

      • Reynald Affeldt, Manabu Hagiwara

      Pages 233-249

8. (Non-)Termination and Automata

   1. Stop When You Are Almost-Full

      • Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt

      Pages 250-265

   2. Certification of Nontermination Proofs

      • Christian Sternagel, René Thiemann

      Pages 266-282

   3. A Compact Proof of Decidability for Regular Expression Equivalence

      • Andrea Asperti

      Pages 283-298

This book constitutes the thoroughly refereed proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, held in Princeton, NJ, USA, in August 2012. The 21 revised full papers presented together with 4 rough diamond papers, 3 invited talks, and one invited tutorial were carefully reviewed and selected from 40 submissions. Among the topics covered are formalization of mathematics; program abstraction and logics; data structures and synthesis; security; (non-)termination and automata; program verification; theorem prover development; reasoning about program execution; and prover infrastructure and modeling styles.

• Coq
• algebra
• formal methods
• monadic programs
• temporal logics

• Department of Computer Science, Princeton University, Princeton, USA

  Lennart Beringer

• School of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, Canada

  Amy Felty

Policies and ethics