↓ Skip to main content

Theorem Proving in Higher Order Logics

Overview of attention for book
Cover of 'Theorem Proving in Higher Order Logics'

Table of Contents

  1. Altmetric Badge
    Book Overview
  2. Altmetric Badge
    Chapter 1 Fix-Point Equations for Well-Founded Recursion in Type Theory
  3. Altmetric Badge
    Chapter 2 Programming and Computing in HOL
  4. Altmetric Badge
    Chapter 3 Proof Terms for Simply Typed Higher Order Logic
  5. Altmetric Badge
    Chapter 4 Routing Information Protocol in HOL/SPIN
  6. Altmetric Badge
    Chapter 5 Recursive Families of Inductive Types
  7. Altmetric Badge
    Chapter 6 Aircraft Trajectory Modeling and Alerting Algorithm Verification
  8. Altmetric Badge
    Chapter 7 Intel’s Formal Verification Experience on the Willamette Development
  9. Altmetric Badge
    Chapter 8 A Prototype Proof Translator from HOL to Coq
  10. Altmetric Badge
    Chapter 9 Proving ML Type Soundness Within Coq
  11. Altmetric Badge
    Chapter 10 On the Mechanization of Real Analysis in Isabelle/HOL
  12. Altmetric Badge
    Chapter 11 Equational Reasoning via Partial Reflection
  13. Altmetric Badge
    Chapter 12 Reachability Programming in HOL98 Using BDDs
  14. Altmetric Badge
    Chapter 13 Transcendental Functions and Continuity Checking in PVS
  15. Altmetric Badge
    Chapter 14 Verified Optimizations for the Intel IA-64 Architecture
  16. Altmetric Badge
    Chapter 15 Formal Verification of IA-64 Division Algorithms
  17. Altmetric Badge
    Chapter 16 Fast Tactic-Based Theorem Proving
  18. Altmetric Badge
    Chapter 17 Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover
  19. Altmetric Badge
    Chapter 18 A Strong and Mechanizable Grand Logic
  20. Altmetric Badge
    Chapter 19 Inheritance in Higher Order Logic: Modeling and Reasoning
  21. Altmetric Badge
    Chapter 20 Total-Correctness Refinement for Sequential Reactive Systems
  22. Altmetric Badge
    Chapter 21 Divider Circuit Verification with Model Checking and Theorem Proving
  23. Altmetric Badge
    Chapter 22 Specification and Verification of a Steam-Boiler with Signal-Coq
  24. Altmetric Badge
    Chapter 23 Functional Procedures in Higher-Order Logic
  25. Altmetric Badge
    Chapter 24 Formalizing Stålmarck’s Algorithm in Coq
  26. Altmetric Badge
    Chapter 25 TAS — A Generic Window Inference System
  27. Altmetric Badge
    Chapter 26 Weak Alternating Automata in Isabelle/HOL
  28. Altmetric Badge
    Chapter 27 Graphical Theories of Interactive Systems: Can a Proof Assistant Help?
  29. Altmetric Badge
    Chapter 28 Formal Verification of the Alpha 21364 Network Protocol
  30. Altmetric Badge
    Chapter 29 Dependently Typed Records for Representing Mathematical Structure
  31. Altmetric Badge
    Chapter 30 Towards a Machine-Checked Java Specification Book
  32. Altmetric Badge
    Chapter 31 Another Look at Nested Recursion
  33. Altmetric Badge
    Chapter 32 Automating the Search for Answers to Open Questions
  34. Altmetric Badge
    Chapter 33 Appendix: Conjectures Concerning Proof, Design, and Verification
Overall attention for this book and its chapters
Altmetric Badge

Mentioned by

wikipedia
1 Wikipedia page

Citations

dimensions_citation
5 Dimensions

Readers on

mendeley
11 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
Theorem Proving in Higher Order Logics
Published by
Springer, Berlin, Heidelberg, January 2000
DOI 10.1007/3-540-44659-1
ISBNs
978-3-54-067863-2, 978-3-54-044659-0
Editors

Mark Aagaard, John Harrison

Mendeley readers

Mendeley readers

The data shown below were compiled from readership statistics for 11 Mendeley readers of this research output. Click here to see the associated Mendeley record.

Geographical breakdown

Country Count As %
Portugal 1 9%
France 1 9%
Brazil 1 9%
Unknown 8 73%

Demographic breakdown

Readers by professional status Count As %
Student > Ph. D. Student 4 36%
Researcher 3 27%
Student > Postgraduate 1 9%
Student > Bachelor 1 9%
Other 1 9%
Other 1 9%
Readers by discipline Count As %
Computer Science 9 82%
Business, Management and Accounting 1 9%
Chemistry 1 9%