Topics - Theorem Provers
Concepts
- Soft Type Systems
- On Kernel Size, or why anything beyond 441 lines of code should be considered "too big" to be considered "small".
- Logical Frameworks
- Meta-logical Frameworks
- HOL family of provers
Specific Proof Assistants
- Automath, one of the first "modern" proof assistants
- Mizar (topics) a lovely proof assistant
- Definitions in Mizar some notes
- Schemes
- Idiomatic Mizar
- Group Theory in Mizar
- Example Definitions in finite group theory
- HOL Light (topics) for a small and elegant implementation of
Higher-order logic
- Compiling HOL Light with a couple "gotchas" on Raspberry Pi (and in general)
- Definitions in HOL Light
- Group Theory in HOL Light
- HOL (topics)
- Coq
- Isabelle (topics)