git @ Cat's Eye Technologies The-Glosscubator / master by-topic / Theorem Proving / ratings / cpressey.md
master

Tree @master (Download .tar.gz)

cpressey.md @masterview markup · raw · history · blame

Ratings by cpressey of Theorem Proving works

The Seventeen Provers of the World

  • rating: 1

.

Theorem Proving in Lean 4

  • rating: 1

.

How to believe a machine-checked proof

  • rating: 1

.

Automated Reasoning and its Applications

  • rating: 0

.

The LCF Approach to Theorem Proving

  • rating: 1

.

From LCF to HOL

  • rating: TODO

.

Automated Reasoning for the Working Mathematician

  • rating: 1

.

The Future of Mathematics?

  • rating: 3

.

HOL Light - tutorial.pdf

  • rating: 1

.

Theorem proving support in programming language semantics

  • rating: 1

.

Towards self-verification of HOL Light

  • rating: TODO

.

A Self-Verifying Theorem Prover

  • rating: TODO

.

The Incredible Proof Machine

  • rating: 3

.

LCF architecture | PLS Lab

  • rating: 1

.

The de Bruijn criterion vs the LCF architecture

  • rating: 1

.

John Harrison: Slides from recent talks

  • rating: 1

.

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

  • rating: 3

.

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

  • rating: 1

.

Robbins Algebras are Boolean

  • rating: 1

.

HOL Interactive Theorem Prover

  • rating: 1
  • useful: true

.

HOL Light

  • rating: 1

.

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

  • rating: 1

.

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

  • rating: 1

.

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

  • rating: 1

.

F* Tutorial

  • rating: 1

.

Calculational proofs · FStarLang/FStar Wiki

  • rating: 1

.

Executing F* code · FStarLang/FStar Wiki

  • rating: 1

.

Proof-oriented Programming in F*

  • rating: 1

.

F* - An introduction to the F* programming language

  • rating: 1

.

Program verification with F*

  • rating: 1

.

Metamath Home Page

  • rating: 1

.

Ulrich Berger, Minlog (wayback)

  • rating: 1

.

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

  • rating: 2

.

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

  • rating: 2

.