View Source Document

Chris Pressey.md

Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Theorem Proving

The Seventeen Provers of the World

There is also a paper by this name. I guess this is the book version of that paper. Compares the same proof written for different theorem provers.

Theorem Proving in Lean 4

Started in 2017 but kept updated.

How to believe a machine-checked proof

Addresses some basic philosophical issues regarding machine-checked proofs.

Automated Reasoning and its Applications

Overall, very introductory.

Compares CAS, automated theorem proving, interactive theorem proving.

Refers to the book "The Seventeen Provers of the World".

Points out that formal verification can prevent expensive disasters, but is itself expensive and is only as reliable as the formal models used. Ends with math, the Flyspeck project.

The LCF Approach to Theorem Proving

The LCF approach is to have an abstract data type representing valid proofs, exposing only those operations which represent valid proof steps, so that the result of each of those operations is also necessarily a valid proof.

From LCF to HOL

.

Automated Reasoning for the Working Mathematician

Lots of discussion on how much automation can or should be used, and when, when formalizing mathematics.

The Future of Mathematics?

Buzzard gives the opinion that, if his work in pure mathematics is neither useful nor 100 percent guaranteed to be correct, then it is surely a waste of time. I find this a striking opinion. I am inclined to agree, and insofar as I do work in formal systems that I do not expect to be useful, I would also be well-pleased if it enjoyed the property of being 100 percent guaranteed to be correct...

HOL Light - tutorial.pdf

.

Theorem proving support in programming language semantics

They formalize the semantics of the simple languages from Winskel's book in Coq, in various approaches to formal semantics: operational, denotational, axiomatic. For the operational semantics, evaluation is stepwise, in an environment, where environments are lists of pairs of names and values. Functions aeval and beval, defined in Coq capture this stepwise reduction. They then briefly consider big-step operational semantics version of this, but note that the big-step reduction function is not total, because the language is Turing-complete. (The function for small-step semantics is also a partial recursive function, but it is structural, and therefore guaranteed to terminate.)

Then comes axiomatic semantics. A verification condition generator for weakest-precondition semantics is considered. The axiomatic semantics is proved correct wrt the operational semantics (reminds me of a monograph from the 70's about using multiple semantical definitions of a programming language; always a good step, for enhancing correctness, IMO.)

When they formalize the denotational semantics, for which Coq's always-total functions are a poor fit, ... this is where we get to see how they propose to encode the partial functions needed for this (and for big-step operational semantics) in Coq.

They use Tarski's fixpoint theorem (p. 17). A partial order is complete if every chain has a least upper bound. A function is continuous if it preserves least upper bounds (if I read that correctly). Tarski's theorem can be formalized in constructive logic, but proving that (partial) functions are cpo's requires non-constructive axioms.

They use a non-constructive operator "proposed by Hilbert and already used in HOL or Isabelle/HOL" which takes an inhabited type and a predicate on that type, and returns a value in the type that satisfies the predicate (if possible), to define a fixpoint operator Tarski_fix, which they use as a "programming tool".

Finally, abstract interpretation. They implement ab_eval which evaluates to an abstract value. It is exactly like the one for axiomatic semantics, just replacing the concrete operation with an abstract notion. The abs interp stuff is largely unsurprising. This departs from "define the semantics" towards "provide tools based on the semantics", which was part of the thesis.

Towards self-verification of HOL Light

.

A Self-Verifying Theorem Prover

.

The Incredible Proof Machine

.

LCF architecture \| PLS Lab

.

The de Bruijn criterion vs the LCF architecture

.

John Harrison: Slides from recent talks

.

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

In 1996, William McCune used the automated theorem prover EQN to show that Robbins algebras are Boolean algebras (i.e. that Robbins' axioms are an alternative axiomatic basis for Boolean algebra).

HOL Interactive Theorem Prover

.

HOL Light

.

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

.

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

.

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*

Lecture notes

F* - An introduction to the F* programming language

.

Program verification with F*

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

Metamath Home Page

.

Ulrich Berger, Minlog (wayback)

.

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

.

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

It leaves me scratching my head, as it's completely undocumented, and I actually suspect this is not a great way to approach the problem that I assume it to be trying to solve - but it's very interesting nonetheless.