Advertisement

Interactive Theorem Proving

Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings

  • Marko van Eekelen
  • Herman Geuvers
  • Julien Schmaltz
  • Freek Wiedijk

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

Table of contents

  1. Front Matter
  2. Invited Papers

    1. Bart Jacobs, Ronny Wichers Schreur
      Pages 3-17
    2. Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov
      Pages 18-21
  3. Regular Papers

    1. Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal
      Pages 22-38
    2. Lennart Beringer
      Pages 39-54
    3. Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza
      Pages 55-70
    4. Renaud Clavel, Laurence Pierre, Régis Leveugle
      Pages 71-86
    5. Georges Gonthier
      Pages 103-118
    6. Sylvain Heraud, David Nowak
      Pages 119-134
    7. Johannes Hölzl, Armin Heller
      Pages 135-151
    8. Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl
      Pages 152-167
    9. Ramana Kumar, Tjark Weber
      Pages 168-183
    10. L. Lambán, F. J. Martín-Mateos, J. Rubio, J. L. Ruiz-Reina
      Pages 200-215
    11. Andreas Lochbihler, Lukas Bulwahn
      Pages 216-232
    12. Tarek Mhamdi, Osman Hasan, Sofiène Tahar
      Pages 233-248
    13. David Monniaux, Pierre Corbineau
      Pages 249-264
    14. Magnus O. Myreen, Jared Davis
      Pages 265-280
    15. Michael Norrish
      Pages 297-311
    16. Peter Reid, Ruben Gamboa
      Pages 312-324
    17. Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, Gerwin Klein
      Pages 325-340
  4. Proof Pearls

    1. Chunhan Wu, Xingyuan Zhang, Christian Urban
      Pages 341-356
  5. Rough Diamonds

    1. Anthony C. J. Fox
      Pages 357-362
    2. Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell
      Pages 363-369
    3. Phil Scott, Jacques Fleuriot
      Pages 370-375
    4. Matej Urbas, Mateja Jamnik
      Pages 376-382
  6. Back Matter

About these proceedings

Introduction

This book constitutes the refereed proceedings of the Second International Conference on Interactive Theorem proving, ITP 2011, held in Berg en Dal, The Netherlands, in August 2011.
The 25 revised full papers presented were carefully reviewed and selected from 50 submissions. Among the topics covered are counterexample generation, verification, validation, term rewriting, theorem proving, computability theory, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc.

Keywords

ACL2 Coq HOL Isabelle formal methods program semantics proof assistants

Editors and affiliations

  • Marko van Eekelen
    • 1
  • Herman Geuvers
    • 2
  • Julien Schmaltz
    • 3
  • Freek Wiedijk
    • 2
  1. 1.Faculteit InformaticaOpen UniversiteitHeerlenThe Netherlands
  2. 2.FNWI/ICIS/ISRadboud Universiteit NijmegenNijmegenThe Netherlands
  3. 3.Faculteit InformaticaOpen UniversiteitHeerlenThe Netherlands

Bibliographic information

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