EEF Foundations school in Deduction and Theorem Proving

Heriot-Watt University, Edinburgh, 6-16 April, 2000

Lecture Notes

ULTRA logo ULTRA group
Useful Logics, Types, Rewriting,
and Applications		 UKII logo UKII
 UK Institute of Informatics,
UK
  • Cover Page
  • Program
  • Contents
  • Interface:
  • David Aspinall: Proof General.
  • Stefano Berardi: The type theory and type checker of GF by Maenpaa and Ranta.
  • Types:
  • Mariangiola Dezani-Ciancaglini: Intersection Types. See in particular
  • Joe Wells: Intersection Types in programming Languages. See this tutorial.
  • Fairouz Kamareddine: Explicit Extensions in Typed Lambda calculi. See these slides.
  • Bob Constable: Types in Logic, Mathematics and Programming. See:
    • Nuprl's Class Theory and its Applications. by Constable and Hickey
    • The Nuprl Open Logical environment (to be scanned, so far only in hard copy). By Allen, Constable, Eaton, Kreitz and Lorigo.
    • Proof Translation Study (to be scanned, so far only in hard copy).
  • Theorem Provers:
  • Larry Paulson: Isabelle.
  • Daniel Hirschkhoff: Coq. See in particular this tutorial by Huet, Kahn and Paulin-Mohring.
  • N.G. de Bruijn: The AUTOMATH System for verification of Mathematics. (to be scanned, so far only in hard copy).
  • Jan van Eijck: Tableaux Theorem Proving for Dynamic First Order Logic. See these notes by van Eijck, Heguiabehere and O' Nuallain
  • Logic, Rewriting and Deduction:
  • Claude Kirchner: Elan and Deduction Modulo.
  • Nicola Olivetti: Algorithmic Proof theory. See these notes by Gabbay and Olivetti
  • Colin Stirling: Modal Logics for Processes. See these notes by Bradfield and Stirling.