Skip to main content
  • Conference proceedings
  • © 2011

Interactive Theorem Proving

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

  • Fast track conference proceedings
  • Unique visibility
  • State of the art research

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

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Conference series link(s): ITP: International Conference on Interactive Theorem Proving

Conference proceedings info: ITP 2011.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (29 papers)

  1. Front Matter

  2. Invited Papers

    1. Logical Formalisation and Analysis of the Mifare Classic Card in PVS

      • Bart Jacobs, Ronny Wichers Schreur
      Pages 3-17
    2. Challenges in Verifying Communication Fabrics

      • Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov
      Pages 18-21
  3. Regular Papers

    1. Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq

      • Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal
      Pages 22-38
    2. Relational Decomposition

      • Lennart Beringer
      Pages 39-54
    3. Structural Analysis of Narratives with the Coq Proof Assistant

      • Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza
      Pages 55-70
    4. Towards Robustness Analysis Using PVS

      • Renaud Clavel, Laurence Pierre, Régis Leveugle
      Pages 71-86
    5. Point-Free, Set-Free Concrete Linear Algebra

      • Georges Gonthier
      Pages 103-118
    6. A Formalization of Polytime Functions

      • Sylvain Heraud, David Nowak
      Pages 119-134
    7. Three Chapters of Measure Theory in Isabelle/HOL

      • Johannes Hölzl, Armin Heller
      Pages 135-151
    8. Termination of Isabelle Functions via Termination of Rewriting

      • Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl
      Pages 152-167
    9. Validating QBF Validity in HOL4

      • Ramana Kumar, Tjark Weber
      Pages 168-183
    10. Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials

      • L. Lambán, F. J. Martín-Mateos, J. Rubio, J. L. Ruiz-Reina
      Pages 200-215
    11. Animating the Formalised Semantics of a Java-Like Language

      • Andreas Lochbihler, Lukas Bulwahn
      Pages 216-232
    12. Formalization of Entropy Measures in HOL

      • Tarek Mhamdi, Osman Hasan, Sofiène Tahar
      Pages 233-248
    13. On the Generation of Positivstellensatz Witnesses in Degenerate Cases

      • David Monniaux, Pierre Corbineau
      Pages 249-264

Other Volumes

  1. Interactive Theorem Proving

About this book

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.

Editors and Affiliations

  • Faculteit Informatica, Open Universiteit, Heerlen, The Netherlands

    Marko Eekelen, Julien Schmaltz

  • FNWI/ICIS/IS, Radboud Universiteit Nijmegen, Nijmegen, The Netherlands

    Herman Geuvers, Freek Wiedijk

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access