Interactive Theorem Proving

Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings

  • Lennart Beringer
  • Amy Felty
Conference proceedings ITP 2012

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

Table of contents

  1. Front Matter
  2. Invited Talks

    1. Lawrence C. Paulson
      Pages 1-10
    2. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin
      Pages 11-27
  3. Invited Tutorial

    1. Andrew Gacek
      Pages 49-50
  4. Formalization of Mathematics I

    1. Maxime Dénès, Anders Mörtberg, Vincent Siles
      Pages 83-98
  5. Program Abstraction and Logics

    1. David Greenaway, June Andronick, Gerwin Klein
      Pages 99-115
    2. Tobias Nipkow
      Pages 116-132
    3. Patrick Michel, Arnd Poetzsch-Heffter
      Pages 133-148
  6. Data Structures and Synthesis

  7. Security

    1. David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring
      Pages 201-216
    2. Xingyuan Zhang, Christian Urban, Chunhan Wu
      Pages 217-232
    3. Reynald Affeldt, Manabu Hagiwara
      Pages 233-249
  8. (Non-)Termination and Automata

    1. Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt
      Pages 250-265
    2. Christian Sternagel, René Thiemann
      Pages 266-282
  9. Program Verification

    1. William Mansky, Elsa L. Gunter
      Pages 299-314
    2. Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal
      Pages 315-331
  10. Rough Diamonds I: Reasoning about Program Execution

    1. Gerwin Klein, Rafal Kolanski, Andrew Boyton
      Pages 332-337
    2. Anthony Fox
      Pages 338-344
  11. Theorem Prover Development

    1. Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
      Pages 345-360
    2. Georges Gonthier, Enrico Tassi
      Pages 361-376
  12. Formalization of Mathematics II

  13. Rough Diamonds II: Prover Infrastructure and Modeling Styles

    1. Ramana Kumar, Joe Hurd
      Pages 405-411
  14. Back Matter

About these proceedings


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

Editors and affiliations

  • Lennart Beringer
    • 1
  • Amy Felty
    • 2
  1. 1.Department of Computer SciencePrinceton UniversityPrincetonUSA
  2. 2.School of Electrical Engineering and Computer ScienceUniversity of OttawaOttawaCanada

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2012
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Computer Science Computer Science (R0)
  • Print ISBN 978-3-642-32346-1
  • Online ISBN 978-3-642-32347-8
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
IT & Software