Theorem Proving

General

• is-heading: true

.

The Incredible Proof Machine

• url: https://incredible.pm/

.

LCF architecture | PLS Lab

• url: https://www.pls-lab.org/LCF_architecture

.

The de Bruijn criterion vs the LCF architecture

• url: https://lawrencecpaulson.github.io/2022/01/05/LCF.html

.

John Harrison: Slides from recent talks

• url: https://www.cl.cam.ac.uk/~jrh13/slides/

.

Satisfiability modulo theories - Wikipedia

• url: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

.

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

• url: https://cs.stackexchange.com/questions/119817/do-theorems-provers-demonstrate-their-own-correctness
• topics: Incompleteness, Theorem Proving

.

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

• url: https://proofassistants.stackexchange.com/questions/2499/what-is-a-deep-embedding-vs-a-shallow-embedding-with-examples.

.

Robbins Algebras are Boolean

• authors: William McCune
• date: 1996
• url: https://www.cs.unm.edu/~mccune/papers/robbins/
• topics: Abstract Algebra, Equational Logic, Theorem Proving

.

HOL (and HOL Light)

• is-heading: true

.

HOL Interactive Theorem Prover

• url: https://hol-theorem-prover.org/

.

HOL Light

• url: https://www.cl.cam.ac.uk/~jrh13/hol-light/

.

HOL Light - Wikipedia

• url: https://en.wikipedia.org/wiki/HOL_Light

.

HOL88/src/ml/hol-rule.ml at master · theoremprover-museum/HOL88

• url: https://github.com/theoremprover-museum/HOL88/blob/master/src/ml/hol-rule.ml

.

Lean

• is-heading: true

.

notes-fplean/notes at cron - notes-fplean - Codeberg.org

• url: https://codeberg.org/dsby/notes-fplean/src/branch/cron/notes

.

F*

• is-heading: true

.

F*: A Higher-Order Effectful Language Designed for Program Verification

• url: https://www.fstar-lang.org/

.

F* Tutorial

• url: http://www.fstar-lang.org/tutorial/

.

Calculational proofs · FStarLang/FStar Wiki

• url: https://github.com/FStarLang/FStar/wiki/Calculational-proofs

.

Executing F* code · FStarLang/FStar Wiki

• url: https://github.com/FStarLang/FStar/wiki/Executing-F%2A-code

.

Proof-oriented Programming in F*

• url: https://fstar-lang.org/gs2021/gs2021.html#/sec-proof-oriented-programming-in-f-

Lecture notes

F* - An introduction to the F* programming language

• url: https://web.archive.org/web/20190609084718/https://rise4fun.com/FStar/tutorialcontent/guide

.

Program verification with F*

• url: https://prosecco.gforge.inria.fr/personal/hritcu/teaching/vtsa2019/

Course at Summer School on Verification Technology, Systems, and Applications, VTSA 2019 at University of Luxembourg on 1-2 July 2019

Other

• is-heading: true

.

Metamath Home Page

• url: https://us.metamath.org/index.html

.

Ulrich Berger, Minlog (wayback)

• url: https://web.archive.org/web/20210506214300/http://www.cs.swan.ac.uk/~csulrich/minlog.html

.