Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings (Lecture Notes in Computer Science Book 9807)

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. Front Matter....Pages I-XVII Front Matter....Pages 1-1 An Isabelle/HOL Formalisation of Green’s Theorem....Pages 3-19 HOL Zero’s Solutions for Pollack-Inconsistency....Pages 20-35 Infeasible Paths Elimination by Symbolic Execution Techniques....Pages 36-51 Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency....Pages 52-68 POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)....Pages 69-86 CoSMed: A Confidentiality-Verified Social Media Platform....Pages 87-106 Mechanical Verification of a Constructive Proof for FLP....Pages 107-122 Visual Theorem Proving with the Incredible Proof Machine....Pages 123-139 Proof Pearl: Bounding Least Common Multiples with Triangles....Pages 140-150 Two-Way Automata in Coq....Pages 151-166 Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms....Pages 167-183 The Flow of ODEs....Pages 184-199 From Types to Sets by Local Type Definitions in Higher-Order Logic....Pages 200-218 Formalizing the Edmonds-Karp Algorithm....Pages 219-234 A Formal Proof of Cauchy’s Residue Theorem....Pages 235-251 Equational Reasoning with Applicative Functors....Pages 252-273 Formally Verified Approximations of Definite Integrals....Pages 274-289 Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems....Pages 290-306 Automatic Functional Correctness Proofs for Functional Search Trees....Pages 307-322 A Framework for the Automatic Formal Verification of Refinement from Cogent to C....Pages 323-340 Front Matter....Pages 1-1 Formalization of the Resolution Calculus for First-Order Logic....Pages 341-357 Verified Operational Transformation for Trees....Pages 358-373 Hereditarily Finite Sets in Constructive Type Theory....Pages 374-390 Algebraic Numbers in Isabelle/HOL....Pages 391-408 Modular Dependent Induction in Coq, Mendler-Style....Pages 409-424 Formalized Timed Automata....Pages 425-440 AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic....Pages 441-456 Front Matter....Pages 457-457 What’s in a Theorem Name?....Pages 459-465 Cardinalities of Finite Relations in Coq....Pages 466-474 Formalising Semantics for Expected Running Time of Probabilistic Programs....Pages 475-482 On the Formalization of Fourier Transform in Higher-order Logic....Pages 483-490 CoqPIE: An IDE Aimed at Improving Proof Development Productivity....Pages 491-499 Back Matter....Pages 501-502