© 2016

Interactive Theorem Proving

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

  • Jasmin Christian Blanchette
  • Stephan Merz
Conference proceedings ITP 2016

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

Also part of the Theoretical Computer Science and General Issues book sub series (LNTCS, volume 9807)

Table of contents

  1. Front Matter
    Pages I-XVII
  2. Regular Contributions

    1. Front Matter
      Pages 1-1
    2. Mohammad Abdulaziz, Lawrence C. Paulson
      Pages 3-19
    3. Romain Aissat, Frédéric Voisin, Burkhart Wolff
      Pages 36-51
    4. June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah
      Pages 52-68
    5. Fahad Ausaf, Roy Dyckhoff, Christian Urban
      Pages 69-86
    6. Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
      Pages 87-106
    7. Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber et al.
      Pages 107-122
    8. Hing-Lun Chan, Michael Norrish
      Pages 140-150
    9. Christian Doczkal, Gert Smolka
      Pages 151-166
    10. Fabian Immler, Christoph Traut
      Pages 184-199
    11. Ondřej Kunčar, Andrei Popescu
      Pages 200-218
    12. Peter Lammich, S. Reza Sefidgar
      Pages 219-234
    13. Wenda Li, Lawrence C. Paulson
      Pages 235-251
    14. Andreas Lochbihler, Joshua Schneider
      Pages 252-273
    15. Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
      Pages 274-289

About these proceedings


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.


distributed systems formal security models logic and verification model checking verification completeness first-order logic formalized mathematics Fourier transform graph transformation higher order logic Isabelle/HOL knowledge representation and reasoning proof assistant semantics software verification soundness symbolic execution theorem proofing type theory

Editors and affiliations

  • Jasmin Christian Blanchette
    • 1
  • Stephan Merz
    • 2
  1. 1.Inria Nancy – Grand EstVillers-lès-NancyFrance
  2. 2.Inria Nancy – Grand EstVillers-lès-NancyFrance

Bibliographic information

Industry Sectors
IT & Software