Skip to main content
SpringerLink
Log in

Interactive Theorem Proving

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

  • Conference proceedings
  • © 2010

Overview

Editors:
  1. Matt Kaufmann

    1. Department of Computer Sciences, University of Texas, Austin, Austin, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Lawrence C. Paulson

    1. Computer Laboratory, University of Cambridge, Cambridge,, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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)

Included in the following conference series:

Conference proceedings info: ITP 2010.

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

Access this book

Log in via an institution
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

Licence this eBook for your library

Institutional subscriptions

Table of contents (35 papers)

  1. Front Matter

    Download chapter PDF

  3. Proof Pearls

    1. A Certified Denotational Abstract Interpreter

      • David Cachera, David Pichardie
      Pages 9-24

    2. Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure

      • John Cowles, Ruben Gamboa
      Pages 25-34

    3. A New Foundation for Nominal Isabelle

      • Brian Huffman, Christian Urban
      Pages 35-50

    4. (Nominal) Unification by Recursive Descent with Triangular Substitutions

      • Ramana Kumar, Michael Norrish
      Pages 51-66

    5. A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks

      • Freek Verbeek, Julien Schmaltz
      Pages 67-82

  4. 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. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

      • Jasmin Christian Blanchette, Tobias Nipkow
      Pages 131-146

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

    6. An Efficient Coq Tactic for Deciding Kleene Algebras

      • Thomas Braibant, Damien Pous
      Pages 163-178

    7. Fast LCF-Style Proof Reconstruction for Z3

      • Sascha Böhme, Tjark Weber
      Pages 179-194

    8. The Optimal Fixed Point Combinator

      • Arthur Charguéraud
      Pages 195-210

    9. Formal Study of Plane Delaunay Triangulation

      • Jean-François Dufourd, Yves Bertot
      Pages 211-226

    10. Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison

      • Amy Felty, Brigitte Pientka
      Pages 227-242

    11. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture

      • Anthony Fox, Magnus O. Myreen
      Pages 243-258

    12. Automated Machine-Checked Hybrid System Safety Proofs

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

Other volumes

  1. Interactive Theorem Proving

Keywords

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

Publish with us

Policies and ethics

Back to top

Search

Navigation