Interactive Theorem Proving

Table of Contents

1. Altmetric Badge
   Book Overview
2. Altmetric Badge
   Chapter 1 An Isabelle/HOL Formalisation of Green’s Theorem
3. Altmetric Badge
   Chapter 2 HOL Zero’s Solutions for Pollack-Inconsistency
4. Altmetric Badge
   Chapter 3 Infeasible Paths Elimination by Symbolic Execution Techniques
5. Altmetric Badge
   Chapter 4 Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency
6. Altmetric Badge
   Chapter 5 POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
7. Altmetric Badge
   Chapter 6 CoSMed: A Confidentiality-Verified Social Media Platform
8. Altmetric Badge
   Chapter 7 Mechanical Verification of a Constructive Proof for FLP
9. Altmetric Badge
   Chapter 8 Visual Theorem Proving with the Incredible Proof Machine
10. Altmetric Badge
    Chapter 9 Proof Pearl: Bounding Least Common Multiples with Triangles
11. Altmetric Badge
    Chapter 10 Two-Way Automata in Coq
12. Altmetric Badge
    Chapter 11 Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
13. Altmetric Badge
    Chapter 12 The Flow of ODEs
14. Altmetric Badge
    Chapter 13 From Types to Sets by Local Type Definitions in Higher-Order Logic
15. Altmetric Badge
    Chapter 14 Formalizing the Edmonds-Karp Algorithm
16. Altmetric Badge
    Chapter 15 A Formal Proof of Cauchy’s Residue Theorem
17. Altmetric Badge
    Chapter 16 Equational Reasoning with Applicative Functors
18. Altmetric Badge
    Chapter 17 Formally Verified Approximations of Definite Integrals
19. Altmetric Badge
    Chapter 18 Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
20. Altmetric Badge
    Chapter 19 Automatic Functional Correctness Proofs for Functional Search Trees
21. Altmetric Badge
    Chapter 20 A Framework for the Automatic Formal Verification of Refinement from Cogent to C
22. Altmetric Badge
    Chapter 21 Formalization of the Resolution Calculus for First-Order Logic
23. Altmetric Badge
    Chapter 22 Verified Operational Transformation for Trees
24. Altmetric Badge
    Chapter 23 Hereditarily Finite Sets in Constructive Type Theory
25. Altmetric Badge
    Chapter 24 Algebraic Numbers in Isabelle/HOL
26. Altmetric Badge
    Chapter 25 Modular Dependent Induction in Coq, Mendler-Style
27. Altmetric Badge
    Chapter 26 Formalized Timed Automata
28. Altmetric Badge
    Chapter 27 AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
29. Altmetric Badge
    Chapter 28 What’s in a Theorem Name?
30. Altmetric Badge
    Chapter 29 Cardinalities of Finite Relations in Coq
31. Altmetric Badge
    Chapter 30 Formalising Semantics for Expected Running Time of Probabilistic Programs
32. Altmetric Badge
    Chapter 31 On the Formalization of Fourier Transform in Higher-order Logic
33. Altmetric Badge
    Chapter 32 CoqPIE: An IDE Aimed at Improving Proof Development Productivity