John Harrison: Slides from recent talks

• Automated Reasoning: A Survey. Logic in Computer Science Block Seminar, Venice International University, 16th March 1998.
• HOL Light and its use in Verification. Third Dutch Proof Tools Day, Utrecht, 6th March 1998.
• Formalizing Dijkstra. Automated Reasoning Talks, Cambridge, 12th Feb 1998.
• Floating point verification: the exponential function. Presented at Intel JF Campus, Portland OR, 8th January 1998, and at the Oregon Graduate Institute, 9th January 1998.
• Floating point verification in HOL Light: the exponential function. Presented for me at AMAST, December 1997.
• Towards HOL2000?. Automated Reasoning Talks, Cambridge, 13th November 1997.
• First Order Logic in Practice. Presented at FTP'97.
• A Prolog Technology Theorem Prover - Mark Stickel (JAR 1988). Presentation at the Automated Reasoning Reading Group!, Cambridge, 26th June 1997.
• Floating point verification: the exponential function. Automated Reasoning Talks, Cambridge, 5th June 1997.
• Verifying Algorithms for the Transcendental Functions. Scottish Applied Theorem Proving Day, St. Andrews, 14th March 1997.
• Automated Reasoning. Cambridge University Computer Society lecture, Cambridge, 22nd January 1997.
• Introduct ion to Functional Programming: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12. Undergraduate lecture course, January - February 1997.
• Proof Automation and Proof Style. Invited talk at 1996 TYPES Working group annual meeting, Aussois, 16th December 1996.
• HOL Light: A Tutorial Introduction. Formal Methods in Computer-Aided Design, system tutorial/demo, Palo Alto, 7th November 1996.
• Theorem Provers and Computer Algebra Systems. University of Cambridge Computer Lab Wednesday Seminar, Cambridge, 2nd November 1994.