Interactive Theorem Proving

1. Regular Contributions

   1. Automatic Functional Correctness Proofs for Functional Search Trees

      • Tobias Nipkow

      Pages 307-322

   2. A Framework for the Automatic Formal Verification of Refinement from Cogent to C

      • Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O’Connor et al.

      Pages 323-340

   3. Formalization of the Resolution Calculus for First-Order Logic

      • Anders Schlichtkrull

      Pages 341-357

   4. Verified Operational Transformation for Trees

      • Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov

      Pages 358-373

   5. Hereditarily Finite Sets in Constructive Type Theory

      • Gert Smolka, Kathrin Stark

      Pages 374-390

   6. Algebraic Numbers in Isabelle/HOL

      • René Thiemann, Akihisa Yamada

      Pages 391-408

   7. Modular Dependent Induction in Coq, Mendler-Style

      • Paolo Torrini

      Pages 409-424

   8. Formalized Timed Automata

      • Simon Wimmer

      Pages 425-440

   9. AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic

      • Bohua Zhan

      Pages 441-456

2. Rough Diamonds

   1. Front Matter

      Pages 457-457

      PDF

   2. What’s in a Theorem Name?

      • David Aspinall, Cezary Kaliszyk

      Pages 459-465

   3. Cardinalities of Finite Relations in Coq

      • Paul Brunet, Damien Pous, Insa Stucke

      Pages 466-474

   4. Formalising Semantics for Expected Running Time of Probabilistic Programs

      • Johannes Hölzl

      Pages 475-482

   5. On the Formalization of Fourier Transform in Higher-order Logic

      • Adnan Rashid, Osman Hasan

      Pages 483-490

   6. CoqPIE: An IDE Aimed at Improving Proof Development Productivity

      • Kenneth Roe, Scott Smith

      Pages 491-499

3. Back Matter

   Pages 501-502

   PDF

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

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

  Jasmin Christian Blanchette, Stephan Merz

Policies and ethics