Skip to main content
SpringerLink
Log in
Book cover

Interactive Theorem Proving

7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings

  • Conference proceedings
  • © 2016

Overview

Editors:
  1. Jasmin Christian Blanchette

    1. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Stephan Merz

    1. Inria Nancy – Grand Est, Villers-lès-Nancy, France

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

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

Included in the following conference series:

Conference proceedings info: ITP 2016.

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

  1. Front Matter

    Pages I-XVII
    Download chapter PDF

  2. Regular Contributions

    1. Front Matter

      Pages 1-1
      Download chapter PDF

    2. An Isabelle/HOL Formalisation of Green’s Theorem

      • Mohammad Abdulaziz, Lawrence C. Paulson
      Pages 3-19

    3. HOL Zero’s Solutions for Pollack-Inconsistency

      • Mark Adams
      Pages 20-35

    4. Infeasible Paths Elimination by Symbolic Execution Techniques

      • Romain Aissat, Frédéric Voisin, Burkhart Wolff
      Pages 36-51

    5. Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency

      • June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah
      Pages 52-68

    6. POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

      • Fahad Ausaf, Roy Dyckhoff, Christian Urban
      Pages 69-86

    7. CoSMed: A Confidentiality-Verified Social Media Platform

      • Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
      Pages 87-106

    8. Mechanical Verification of a Constructive Proof for FLP

      • Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber et al.
      Pages 107-122

    9. Visual Theorem Proving with the Incredible Proof Machine

      • Joachim Breitner
      Pages 123-139

    10. Proof Pearl: Bounding Least Common Multiples with Triangles

      • Hing-Lun Chan, Michael Norrish
      Pages 140-150

    11. Two-Way Automata in Coq

      • Christian Doczkal, Gert Smolka
      Pages 151-166

    12. Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

      • Thomas Grégoire, Adam Chlipala
      Pages 167-183

    13. The Flow of ODEs

      • Fabian Immler, Christoph Traut
      Pages 184-199

    14. From Types to Sets by Local Type Definitions in Higher-Order Logic

      • Ondřej Kunčar, Andrei Popescu
      Pages 200-218

    15. Formalizing the Edmonds-Karp Algorithm

      • Peter Lammich, S. Reza Sefidgar
      Pages 219-234

    16. A Formal Proof of Cauchy’s Residue Theorem

      • Wenda Li, Lawrence C. Paulson
      Pages 235-251

    17. Equational Reasoning with Applicative Functors

      • Andreas Lochbihler, Joshua Schneider
      Pages 252-273

    18. Formally Verified Approximations of Definite Integrals

      • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
      Pages 274-289

    19. Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems

      • Julian Nagele, Aart Middeldorp
      Pages 290-306
Back to top

Other volumes

  1. Interactive Theorem Proving

Keywords

About this book

This book constitutes the refereed proceedings of the 7th International Conference on Interactive Theorem Proving, ITP 2016, held in Nancy, France, in August 2016.


The 27 full papers and 5 short papers presented were carefully reviewed and selected from 55 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematical theories.

Editors and Affiliations

  • Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Jasmin Christian Blanchette, Stephan Merz

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation