aqjune/hol-light-materials

Online materials for HOL-Light

hol-light-materials

Contents

• An overview of HOL Light
• HOL Light Setup

1. How-to

• Use or update assumptions in HOL Light
• Use rewrite tactics well
• Evaluate expressions
• Write your own tactic
• Debug a proof and tactic
• Prove 'trivial' goals

2. More Details

• OCaml data structure of HOL Light
• How does tactic work?
• HOL Light vs. Coq comparison

3. Examples and Exercises

• exercises: exercises for HOL Light
• s2n-bignum tutorial at https://github.com/awslabs/s2n-bignum/tree/main/arm/tutorial

4. Other Online Materials

• Tutorial
• HOL Light: an overview
• Reference Manual (pdf, html)
• Very Quick Reference (pdf, txt)

Misc