↓ Skip to main content

Interactive Theorem Proving

Overview of attention for book
Cover of 'Interactive Theorem Proving'

Table of Contents

  1. Altmetric Badge
    Book Overview
  2. Altmetric Badge
    Chapter 1 Microcode Verification – Another Piece of the Microprocessor Verification Puzzle
  3. Altmetric Badge
    Chapter 2 Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK
  4. Altmetric Badge
    Chapter 3 Towards a Formally Verified Proof Assistant
  5. Altmetric Badge
    Chapter 4 Implicational Rewriting Tactics in HOL
  6. Altmetric Badge
    Chapter 5 A Heuristic Prover for Real Inequalities
  7. Altmetric Badge
    Chapter 6 A Formal Library for Elliptic Curves in the Coq Proof Assistant
  8. Altmetric Badge
    Chapter 7 Truly Modular (Co)datatypes for Isabelle/HOL
  9. Altmetric Badge
    Chapter 8 Cardinals in Isabelle/HOL
  10. Altmetric Badge
    Chapter 9 Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
  11. Altmetric Badge
    Chapter 10 Showing Invariance Compositionally for a Process Algebra for Network Protocols
  12. Altmetric Badge
    Chapter 11 A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
  13. Altmetric Badge
    Chapter 12 From Operational Models to Information Theory; Side Channels in pGCL with Isabelle
  14. Altmetric Badge
    Chapter 13 A Coq Formalization of Finitely Presented Modules
  15. Altmetric Badge
    Chapter 14 Formalized, Effective Domain Theory in Coq
  16. Altmetric Badge
    Chapter 15 Completeness and Decidability Results for CTL in Coq
  17. Altmetric Badge
    Chapter 16 Hypermap Specification and Certified Linked Implementation Using Orbits
  18. Altmetric Badge
    Chapter 17 A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
  19. Altmetric Badge
    Chapter 18 Experience Implementing a Performant Category-Theory Library in Coq
  20. Altmetric Badge
    Chapter 19 Interactive Theorem Proving
  21. Altmetric Badge
    Chapter 20 Interactive Theorem Proving
  22. Altmetric Badge
    Chapter 21 Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
  23. Altmetric Badge
    Chapter 22 Recursive Functions on Lazy Lists via Domains and Topologies
  24. Altmetric Badge
    Chapter 23 Formal Verification of Optical Quantum Flip Gate
  25. Altmetric Badge
    Chapter 24 Compositional Computational Reflection
  26. Altmetric Badge
    Chapter 25 An Isabelle Proof Method Language
  27. Altmetric Badge
    Chapter 26 Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
  28. Altmetric Badge
    Chapter 27 Interactive Theorem Proving
  29. Altmetric Badge
    Chapter 28 Balancing Lists: A Proof Pearl
  30. Altmetric Badge
    Chapter 29 Unified Decision Procedures for Regular Expression Equivalence
  31. Altmetric Badge
    Chapter 30 Collaborative Interactive Theorem Proving with Clide
  32. Altmetric Badge
    Chapter 31 On the Formalization of Z-Transform in HOL
  33. Altmetric Badge
    Chapter 32 Universe Polymorphism in Coq
  34. Altmetric Badge
    Chapter 33 Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
  35. Altmetric Badge
    Chapter 34 HOL Constant Definition Done Right
  36. Altmetric Badge
    Chapter 35 Rough Diamond: An Extension of Equivalence-Based Rewriting
  37. Altmetric Badge
    Chapter 36 Formal C Semantics: CompCert and the C Standard
  38. Altmetric Badge
    Chapter 37 Mechanical Certification of Loop Pipelining Transformations: A Preview
Overall attention for this book and its chapters
Altmetric Badge

Mentioned by

blogs
1 blog
twitter
3 tweeters

Citations

dimensions_citation
5 Dimensions
You are seeing a free-to-access but limited selection of the activity Altmetric has collected about this research output. Click here to find out more.
Title
Interactive Theorem Proving
Published by
Springer International Publishing, June 2014
DOI 10.1007/978-3-319-08970-6
ISBNs
978-3-31-908969-0, 978-3-31-908970-6
Editors

Klein, Gerwin, Gamboa, Ruben

Twitter Demographics

The data shown below were collected from the profiles of 3 tweeters who shared this research output. Click here to find out more about how the information was compiled.