Skip to main content
SpringerLink
Log in

Interactive Theorem Proving

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

  • Conference proceedings
  • © 2015

Overview

Editors:
  1. Christian Urban

    1. Department of Informatics, King's College London, London, United Kingdom

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Xingyuan Zhang

    1. PLA University of Science and Technology, Nanjing, China

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

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Included in the following conference series:

Conference proceedings info: ITP 2015.

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

Licence this eBook for your library

Institutional subscriptions

Table of contents (30 papers)

  1. Front Matter

    Pages I-XI
    Download chapter PDF

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

    • Mohammad Abdulaziz, Charles Gretton, Michael Norrish
    Pages 1-16

  3. Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory

    • Reynald Affeldt, Jacques Garrigue
    Pages 17-33

  4. ROSCoq: Robots Powered by Constructive Reals

    • Abhishek Anand, Ross Knepper
    Pages 34-50

  5. Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface

    • Bruno Barras, Carst Tankink, Enrico Tassi
    Pages 51-66

  6. A Concrete Memory Model for CompCert

    • Frédéric Besson, Sandrine Blazy, Pierre Wilke
    Pages 67-83

  7. Validating Dominator Trees for a Fast, Verified Dominance Test

    • Sandrine Blazy, Delphine Demange, David Pichardie
    Pages 84-99

  8. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra

    • Sylvain Boulmé, Alexandre Maréchal
    Pages 100-116

  9. Mechanisation of AKS Algorithm: Part 1 – The Main Theorem

    • Hing-Lun Chan, Michael Norrish
    Pages 117-136

  10. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

    • Arthur Charguéraud, François Pottier
    Pages 137-153

  11. Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker

    • Luís Cruz-Filipe, Peter Schneider-Kamp
    Pages 154-169

  12. Proof-Producing Reflection for HOL

    • Benja Fallenstein, Ramana Kumar
    Pages 170-186

  13. Improved Tool Support for Machine-Code Decompilation in HOL4

    • Anthony Fox
    Pages 187-202

  14. A Formalized Hierarchy of Probabilistic System Types

    • Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
    Pages 203-220

  15. A Verified Enclosure for the Lorenz Attractor (Rough Diamond)

    • Fabian Immler
    Pages 221-226

  16. Learning to Parse on Aligned Corpora (Rough Diamond)

    • Cezary Kaliszyk, Josef Urban, Jiří Vyskočil
    Pages 227-233

  17. A Consistent Foundation for Isabelle/HOL

    • Ondřej Kunčar, Andrei Popescu
    Pages 234-252

  18. Refinement to Imperative/HOL

    • Peter Lammich
    Pages 253-269

  19. Stream Fusion for Isabelle’s Code Generator

    • Andreas Lochbihler, Alexandra Maximova
    Pages 270-277

  20. HOCore in Coq

    • Petar Maksimović, Alan Schmitt
    Pages 278-293
Back to top

Other volumes

  1. Interactive Theorem Proving

Keywords

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

Publish with us

Policies and ethics

Back to top

Search

Navigation