Skip to main content
SpringerLink
Log in
Book cover
  • Conference proceedings
  • © 2014

Interactive Theorem Proving

5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings

Editors:

  1. Gerwin Klein

    1. NICTA, Sydney, Australia

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Ruben Gamboa

    1. University of Wyoming, Laramie, USA

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

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

Sections

Buy it now

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 (37 papers)

  1. Front Matter

    PDF

  2. Invited Papers

    2. Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK

      • Roderick Chapman, Florian Schanda
      Pages 17-26

  3. Regular Papers

    1. Towards a Formally Verified Proof Assistant

      • Abhishek Anand, Vincent Rahli
      Pages 27-44

    2. Implicational Rewriting Tactics in HOL

      • Vincent Aravantinos, Sofiène Tahar
      Pages 45-60

    3. A Heuristic Prover for Real Inequalities

      • Jeremy Avigad, Robert Y. Lewis, Cody Roux
      Pages 61-76

    4. A Formal Library for Elliptic Curves in the Coq Proof Assistant

      • Evmorfia-Iro Bartzia, Pierre-Yves Strub
      Pages 77-92

    5. Truly Modular (Co)datatypes for Isabelle/HOL

      • Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
      Pages 93-110

    6. Cardinals in Isabelle/HOL

      • Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
      Pages 111-127

    7. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code

      • Sandrine Blazy, Vincent Laporte, David Pichardie
      Pages 128-143

    8. Showing Invariance Compositionally for a Process Algebra for Network Protocols

      • Timothy Bourke, Robert J. van Glabbeek, Peter Höfner
      Pages 144-159

    9. A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)

      • Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
      Pages 160-176

    11. A Coq Formalization of Finitely Presented Modules

      • Cyril Cohen, Anders Mörtberg
      Pages 193-208

    12. Formalized, Effective Domain Theory in Coq

      • Robert Dockins
      Pages 209-225

    13. Completeness and Decidability Results for CTL in Coq

      • Christian Doczkal, Gert Smolka
      Pages 226-241

    15. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction

      • Kento Emoto, Frédéric Loulergue, Julien Tesson
      Pages 258-274

    16. Experience Implementing a Performant Category-Theory Library in Coq

      • Jason Gross, Adam Chlipala, David I. Spivak
      Pages 275-291

    17. A New and Formalized Proof of Abstract Completion

      • Nao Hirokawa, Aart Middeldorp, Christian Sternagel
      Pages 292-307
Back to top

Other Volumes

  1. Interactive Theorem Proving

Back to top

About this book

This book constitutes the proceedings of the 5th International Conference on Interactive Theorem Proving, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 35 papers presented in this volume were carefully reviewed and selected from 59 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics.
Back to top

Keywords

Back to top

Editors and Affiliations

  • NICTA, Sydney, Australia

    Gerwin Klein

  • University of Wyoming, Laramie, USA

    Ruben Gamboa

Back to top

Bibliographic Information

Back to top

Publish with us

Policies and ethics

Back to top
Access via your institution

Buy it now

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

Search

Navigation