Results Proved in HOL
- See textbook by Andrews for definitions of number theory in HOL
- Isabelle Archive of Formal proofs containing:
- semantics and type soundness of Java
- cryptographic primitives and systems
- real analysis theorems and inequalities
- category theory
- completeness theorem for FOL
- AVL trees, binary search trees
- correctness of compilation techniques
- Fast Fourier Transform correctness
- distributed algorithms (clock synchronization, disk paxos)
- quantifier elimination
- In HOL system
- Also results in variations of HOL implemented in systems PVS, Coq, NuPRL