Theorem Proving Papers

How to believe a machine-checked proof

• authors: Robert Pollack
• date: July 1997
• publication: BRICS
• online @ tidsskrift.dk

.

Automated Reasoning and its Applications

• authors: John Harrison (Intel Corporation)
• date: 30 July 2009
• publication: slides from a talk in Hanoi
• online @ www.cl.cam.ac.uk

.

The LCF Approach to Theorem Proving

• authors: John Harrison
• date: September 2001
• publication: slides from a talk given at the University of Manchester
• online @ www.cl.cam.ac.uk

.

From LCF to HOL

• subtitle: a short history
• authors: Mike Gordon
• date: 2000
• online @ www.cl.cam.ac.uk
• publication: Proof, Language, and Interaction, by G. Plotkin (Editor), Colin P. Stirling (Editor), Mads Tofte (Editor). MIT Press, 2000; ISBN: 0262161885

.

Automated Reasoning for the Working Mathematician

• authors: Jeremy Avigad
• date: 2019
• publication: slides from a talk given in London
• online @ www.contrib.andrew.cmu.edu

.

The Future of Mathematics?

• authors: Kevin Buzzard
• date: January 2020
• publication: slides from a talk given at Pittsburgh
• online @ www.andrew.cmu.edu

.

HOL Light - tutorial.pdf

• authors: John Harrison
• date: 2017
• online @ www.cl.cam.ac.uk

.

Theorem proving support in programming language semantics

• authors: Yves Bertot
• date: 2007
• online @ arxiv.org
• topics: Theorem Proving, Coq, PLDI
• future-topics: Formal Semantics, Operational Semantics, Denotational Semantics, Axiomatic Semantics, Abstract Interpretation

.

Towards self-verification of HOL Light

• authors: John Harrison
• date: 2003??
• online @ www.cl.cam.ac.uk
• topics: Theorem Proving
• future-topics: Self-Verification

.

A Self-Verifying Theorem Prover

• authors: Jared Curran Davis
• date: 2009
• online @ www.kookamara.com
• topics: Theorem Proving
• future-topics: Self-Verification

.