Skip to main content
SpringerLink
Log in
Download book PDF
Book cover
  • Conference proceedings
  • © 2013

Interactive Theorem Proving

4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings

Editors:

  1. Sandrine Blazy

    1. IRISA, Université Rennes 1, Rennes Cedex, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Christine Paulin-Mohring

    1. Université Paris-Sud, LRI, Bat 650, Univ. Paris Sud, Orsay Cedex, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. David Pichardie

    1. Inria Rennes-Bretagne Atlantique, Rennes Cedex, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Fast-track conference proceedings of ITP 2013

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

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

Sections

Buy it now

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

Table of contents (38 papers)

  1. Front Matter

    PDF

  2. Invited Talks

    1. Applying Formal Methods in the Large

      • Dominique Bolignano
      Pages 1-1
      PDF

    2. Automating Theorem Proving with SMT

      • K. Rustan M. Leino
      Pages 2-16
      PDF

    3. Certifying Voting Protocols

      • Carsten Schürmann
      Pages 17-17
      PDF

  4. Regular Papers

    1. MaSh: Machine Learning for Sledgehammer

      • Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban
      Pages 35-50
      PDF

    2. Scalable LCF-Style Proof Translation

      • Cezary Kaliszyk, Alexander Krauss
      Pages 51-66
      PDF

    3. Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation

      • Guillaume Claret, Lourdes del Carmen González Huesca, Yann Régis-Gianas, Beta Ziliani
      Pages 67-83
      PDF

    4. Automatic Data Refinement

      • Peter Lammich
      Pages 84-99
      PDF

    5. Data Refinement in Isabelle/HOL

      • Florian Haftmann, Alexander Krauss, Ondřej Kunčar, Tobias Nipkow
      Pages 100-115
      PDF
    6. PDF

    7. Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1

      • Michael Norrish, Brian Huffman
      Pages 133-146
      PDF

    8. Mechanising Turing Machines and Computability Theory in Isabelle/HOL

      • Jian Xu, Xingyuan Zhang, Christian Urban
      Pages 147-162
      PDF

    9. A Machine-Checked Proof of the Odd Order Theorem

      • Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot et al.
      Pages 163-179
      PDF
    10. PDF

    11. Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL

      • Alasdair Armstrong, Georg Struth, Tjark Weber
      Pages 197-212
      PDF

    12. Pragmatic Quotient Types in Coq

      • Cyril Cohen
      Pages 213-228
      PDF

    13. Mechanical Verification of SAT Refutations with Extended Resolution

      • Nathan Wetzler, Marijn J. H. Heule, Warren A. Hunt Jr.
      Pages 229-244
      PDF

    14. Formalizing Bounded Increase

      • René Thiemann
      Pages 245-260
      PDF
Back to top

Other Volumes

  1. Interactive Theorem Proving

Back to top

About this book

This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.
Back to top

Keywords

Back to top

Editors and Affiliations

  • IRISA, Université Rennes 1, Rennes Cedex, France

    Sandrine Blazy

  • Université Paris-Sud, LRI, Bat 650, Univ. Paris Sud, Orsay Cedex, France

    Christine Paulin-Mohring

  • Inria Rennes-Bretagne Atlantique, Rennes Cedex, France

    David Pichardie

Back to top

Bibliographic Information

Back to top

Publish with us

Policies and ethics

Back to top
Download book PDF

Buy it now

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

Search

Navigation