Theorem Proving
(Up) | See also: Formal Specification, Coq
Web resources
General
The Incredible Proof Machine ★★★
The de Bruijn criterion vs the LCF architecture ★
John Harrison: Slides from recent talks ★
Satisfiability modulo theories - Wikipedia
Robbins Algebras are Boolean ★ 💭
HOL (and HOL Light)
HOL Interactive Theorem Prover ★
HOL88/src/ml/hol-rule.ml at master · theoremprover-museum/HOL88 ★
Lean
notes-fplean/notes at cron - notes-fplean - Codeberg.org ★
F*
F*: A Higher-Order Effectful Language Designed for Program Verification ★
Calculational proofs · FStarLang/FStar Wiki ★
Executing F* code · FStarLang/FStar Wiki ★
Proof-oriented Programming in F* ★ 💭
F* - An introduction to the F* programming language ★
Program verification with F* ★ 💭
Other
Ulrich Berger, Minlog (wayback) ★
Repositories
stepchowfun/proofs: My personal repository of formally verified mathematics. ★★
thautwarm/Sequent.jl: formally and easily, describe the semantics. ★★ 💭
(in Name Binding) bacam/sato-maps-agda ★ 💭
Papers
How to believe a machine-checked proof (online @ tidsskrift.dk) ★ 💭
Automated Reasoning and its Applications (online @ www.cl.cam.ac.uk) 💭
The LCF Approach to Theorem Proving (online @ www.cl.cam.ac.uk) ★ 💭
From LCF to HOL (online @ www.cl.cam.ac.uk)
Automated Reasoning for the Working Mathematician (online @ www.contrib.andrew.cmu.edu) ★ 💭
The Future of Mathematics? (online @ www.andrew.cmu.edu) ★★★ 💭
HOL Light - tutorial.pdf (online @ www.cl.cam.ac.uk) ★
Theorem proving support in programming language semantics (online @ arxiv.org) ★ 💭
Towards self-verification of HOL Light (online @ www.cl.cam.ac.uk)
A Self-Verifying Theorem Prover (online @ www.kookamara.com)
Books
The Seventeen Provers of the World (borrow @ archive.org) ★ 💭
Theorem Proving in Lean 4 (online @ archive.org) ★ 💭