Skip to main content
  • Conference proceedings
  • © 2015

Interactive Theorem Proving

6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings

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

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

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and 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 (30 papers)

  1. Front Matter

    Pages I-XI
  2. Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems

    • Mohammad Abdulaziz, Charles Gretton, Michael Norrish
    Pages 1-16
  3. ROSCoq: Robots Powered by Constructive Reals

    • Abhishek Anand, Ross Knepper
    Pages 34-50
  4. Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface

    • Bruno Barras, Carst Tankink, Enrico Tassi
    Pages 51-66
  5. A Concrete Memory Model for CompCert

    • Frédéric Besson, Sandrine Blazy, Pierre Wilke
    Pages 67-83
  6. Validating Dominator Trees for a Fast, Verified Dominance Test

    • Sandrine Blazy, Delphine Demange, David Pichardie
    Pages 84-99
  7. Mechanisation of AKS Algorithm: Part 1 – The Main Theorem

    • Hing-Lun Chan, Michael Norrish
    Pages 117-136
  8. Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker

    • Luís Cruz-Filipe, Peter Schneider-Kamp
    Pages 154-169
  9. Proof-Producing Reflection for HOL

    • Benja Fallenstein, Ramana Kumar
    Pages 170-186
  10. A Formalized Hierarchy of Probabilistic System Types

    • Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
    Pages 203-220
  11. Learning to Parse on Aligned Corpora (Rough Diamond)

    • Cezary Kaliszyk, Josef Urban, Jiří Vyskočil
    Pages 227-233
  12. A Consistent Foundation for Isabelle/HOL

    • Ondřej Kunčar, Andrei Popescu
    Pages 234-252
  13. Refinement to Imperative/HOL

    • Peter Lammich
    Pages 253-269
  14. Stream Fusion for Isabelle’s Code Generator

    • Andreas Lochbihler, Alexandra Maximova
    Pages 270-277
  15. HOCore in Coq

    • Petar Maksimović, Alan Schmitt
    Pages 278-293

Other Volumes

  1. Interactive Theorem Proving

About this book

This book constitutes the proceedings of the 6th International Conference on Interactive Theorem Proving, ITP 2015, held in Nanjing, China, in August 2015. The 27 papers presented in this volume were carefully reviewed and selected from 54 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics.

Editors and Affiliations

  • Department of Informatics, King's College London, London, United Kingdom

    Christian Urban

  • PLA University of Science and Technology, Nanjing, China

    Xingyuan Zhang

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and 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