All the slides linked here are PDF files. Although your browser may be able to display a PDF, generally they will look better if you open them in Adobe Reader. Therefore, rather than just clicking the links to the slides, you may want to right-click it and download, then double-click the downloaded file to open it in Adobe Reader.
Once you open the PDF file in Adobe Reader, choose View | Full Screen, and then press Enter to advance to the next slidex.
I gave this one-hour talk several times:
Tarskian Geometry and Ruler-and-compass constructions
I gave this one-hour talk at the Stanford Logic Seminar, April 15, 2014.
Proof and Computation in Geometry
I gave this 60-minute talk in Edinburgh, UK, September 19, 2012, at a conference on Automated Deduction in Geometry.
Logic of Ruler and Compass Constructions
I gave this fifteen-minute talk in Cambridge, England, June 19, 2012.
Foundations of Constructive Geometry
I gave this ten-minute talk at the AMS meeting in Boston, January, 2012.
The Parallel Postulate in Constructive Geometry
I gave this talk at the Symposium on Constructive Geometry, Stanford, October 24, 2009. For further background see the talk on Constructive Geometry linked below.
Finiteness in Plateau's Problem
I gave this talk at the Bay Area Differential Geometry Seminar, Stanford, January 31, 2009. The last section was updated in 2015.
Mathematical Logic and Computers: some interesting examples
I gave this talk in Kobe, Japan, on August 31, 2008.
Versions of this talk were given in Leiden, January 2007, and in the Stanford Logic Seminar, February 2007. These slides are a long version, presenting the state of the work in August, 2008. A shortened version was given in Kobe, Japan, in September, 2008.
The Meaning of Existence
I gave this talk at a meeting of the MAA in August, 2007, in San José, California, and again at the Philosophy Department Colloquium in San José in March, 2009.
The Mechanization of Mathematics
I gave this talk at a meeting of the BAMA (Bay Area Mathematics Association) in October, 2005.
Constructibility, Computability, and the Continuum.
I gave this talk at the Stanford ASL meeting, March 2005.
Implicit Typing in Lambda Logic
I gave this talk at the ESHOL workshop of the Logic Programming and Automated Reasoning (LPAR-12) meeting in Jamaica, 2005.
Automatic Derivation of the Equation of Motion of a Pendulum
I gave this talk at the Stanford Artificial Intelligence Seminar in April, 1987; and again at the UCSC math colloquium in May, 1987; but somehow never got around to publishing the work. Now the original computer program seems to be lost.