Skip to main content
  • Conference proceedings
  • © 2010

Interactive Theorem Proving

First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings

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

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 2010.

Buy it now

Buying options

eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.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 (35 papers)

  1. Front Matter

  2. Proof Pearls

    1. A Certified Denotational Abstract Interpreter

      • David Cachera, David Pichardie
      Pages 9-24
    2. A New Foundation for Nominal Isabelle

      • Brian Huffman, Christian Urban
      Pages 35-50
  3. Regular Papers

    1. Extending Coq with Imperative Features and Its Application to SAT Verification

      • Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry
      Pages 83-98
    2. A Tactic Language for Declarative Proofs

      • Serge Autexier, Dominik Dietrich
      Pages 99-114
    3. Programming Language Techniques for Cryptographic Proofs

      • Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin
      Pages 115-130
    4. Formal Proof of a Wave Equation Resolution Scheme: The Method Error

      • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
      Pages 147-162
    5. An Efficient Coq Tactic for Deciding Kleene Algebras

      • Thomas Braibant, Damien Pous
      Pages 163-178
    6. Fast LCF-Style Proof Reconstruction for Z3

      • Sascha Böhme, Tjark Weber
      Pages 179-194
    7. The Optimal Fixed Point Combinator

      • Arthur Charguéraud
      Pages 195-210
    8. Formal Study of Plane Delaunay Triangulation

      • Jean-François Dufourd, Yves Bertot
      Pages 211-226
    9. Automated Machine-Checked Hybrid System Safety Proofs

      • Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen
      Pages 259-274

Other Volumes

  1. Interactive Theorem Proving

Editors and Affiliations

  • Department of Computer Sciences, University of Texas, Austin, Austin, USA

    Matt Kaufmann

  • Computer Laboratory, University of Cambridge, Cambridge,, UK

    Lawrence C. Paulson

Bibliographic Information

Buy it now

Buying options

eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.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