↓ 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 Automated Theory Exploration for Interactive Theorem Proving:
  3. Altmetric Badge
    Chapter 2 Automating Formalization by Statistical and Semantic Parsing of Mathematics
  4. Altmetric Badge
    Chapter 3 A Formalization of Convex Polyhedra Based on the Simplex Method
  5. Altmetric Badge
    Chapter 4 A Formal Proof of the Expressiveness of Deep Learning
  6. Altmetric Badge
    Chapter 5 Formalization of the Lindemann-Weierstrass Theorem
  7. Altmetric Badge
    Chapter 6 CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics
  8. Altmetric Badge
    Chapter 7 Formal Verification of a Floating-Point Expansion Renormalization Algorithm
  9. Altmetric Badge
    Chapter 8 How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
  10. Altmetric Badge
    Chapter 9 FoCaLiZe and Dedukti to the Rescue for Proof Interoperability
  11. Altmetric Badge
    Chapter 10 A Formal Proof in Coq of LaSalle’s Invariance Principle
  12. Altmetric Badge
    Chapter 11 How to Get More Out of Your Oracles
  13. Altmetric Badge
    Chapter 12 Certifying Standard and Stratified Datalog Inference Engines in SSReflect
  14. Altmetric Badge
    Chapter 13 Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
  15. Altmetric Badge
    Chapter 14 Bellerophon: Tactical Theorem Proving for Hybrid Systems
  16. Altmetric Badge
    Chapter 15 Formalizing Basic Quaternionic Analysis
  17. Altmetric Badge
    Chapter 16 A Formalized General Theory of Syntax with Bindings
  18. Altmetric Badge
    Chapter 17 Proof Certificates in PVS
  19. Altmetric Badge
    Chapter 18 Efficient, Verified Checking of Propositional Proofs
  20. Altmetric Badge
    Chapter 19 Proof Tactics for Assertions in Separation Logic
  21. Altmetric Badge
    Chapter 20 Categoricity Results for Second-Order ZF in Dependent Type Theory
  22. Altmetric Badge
    Chapter 21 Making PVS Accessible to Generic Services by Interpretation in a Universal Format
  23. Altmetric Badge
    Chapter 22 Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics
  24. Altmetric Badge
    Chapter 23 Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms
  25. Altmetric Badge
    Chapter 24 Typing Total Recursive Functions in Coq
  26. Altmetric Badge
    Chapter 25 Effect Polymorphism in Higher-Order Logic (Proof Pearl)
  27. Altmetric Badge
    Chapter 26 Schulze Voting as Evidence Carrying Computation
  28. Altmetric Badge
    Chapter 27 Verified Spilling and Translation Validation with Repair
  29. Altmetric Badge
    Chapter 28 A Verified Generational Garbage Collector for CakeML
  30. Altmetric Badge
    Chapter 29 A Formalisation of Consistent Consequence for Boolean Equation Systems
  31. Altmetric Badge
    Chapter 30 Homotopy Type Theory in Lean
  32. Altmetric Badge
    Chapter 31 Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology
  33. Altmetric Badge
    Chapter 32 Formalization of the Fundamental Group in Untyped Set Theory Using Auto2
Overall attention for this book and its chapters
Altmetric Badge

Mentioned by

policy
1 policy source
twitter
11 X users

Citations

dimensions_citation
1 Dimensions

Readers on

mendeley
3 Mendeley
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, Cham, January 2017
DOI 10.1007/978-3-319-66107-0
ISBNs
978-3-31-966106-3, 978-3-31-966107-0
Editors

Mauricio Ayala-Rincón, César A. Muñoz

X Demographics

X Demographics

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