Theorem Proving

(Up) | See also: Formal Specification, Coq

---

Web resources

General

The Incredible Proof Machine

LCF architecture | PLS Lab

The de Bruijn criterion vs the LCF architecture

John Harrison: Slides from recent talks

Satisfiability modulo theories - Wikipedia

formal methods - Do theorems provers demonstrate their own correctness\"? - Computer Science Stack Exchange

translating - What is a deep embedding vs a shallow embedding? With examples? - Proof Assistants Stack Exchange

Robbins Algebras are Boolean

HOL (and HOL Light)

HOL Interactive Theorem Prover

HOL Light

HOL Light - Wikipedia

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

F* Tutorial

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

Metamath Home Page

Ulrich Berger, Minlog (wayback)

Repositories

stepchowfun/proofs: My personal repository of formally verified mathematics.

thautwarm/Sequent.jl: formally and easily, describe the semantics.

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)