Skip to main content
SpringerLink
Log in

Interactive Theorem Proving

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

  • Conference proceedings
  • © 2013

Overview

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)

Included in the following conference series:

Conference proceedings info: ITP 2013.

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

Licence this eBook for your library

Institutional subscriptions

Table of contents (38 papers)

  1. Front Matter

    Download chapter PDF

  2. Invited Talks

    1. Applying Formal Methods in the Large

      • Dominique Bolignano
      Pages 1-1

    2. Automating Theorem Proving with SMT

      • K. Rustan M. Leino
      Pages 2-16

    3. Certifying Voting Protocols

      • Carsten Schürmann
      Pages 17-17

  4. Regular Papers

    1. MaSh: Machine Learning for Sledgehammer

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

    2. Scalable LCF-Style Proof Translation

      • Cezary Kaliszyk, Alexander Krauss
      Pages 51-66

    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

    4. Automatic Data Refinement

      • Peter Lammich
      Pages 84-99

    5. Data Refinement in Isabelle/HOL

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

    6. Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable

      • Andreas Lochbihler
      Pages 116-132

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

      • Michael Norrish, Brian Huffman
      Pages 133-146

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

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

    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

    10. Kleene Algebra with Tests and Coq Tools for while Programs

      • Damien Pous
      Pages 180-196

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

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

    12. Pragmatic Quotient Types in Coq

      • Cyril Cohen
      Pages 213-228

    13. Mechanical Verification of SAT Refutations with Extended Resolution

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

    14. Formalizing Bounded Increase

      • René Thiemann
      Pages 245-260
Back to top

Other volumes

  1. Interactive Theorem Proving

Keywords

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.

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

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation