Merging HOL with Set Theory (Talk)

Overhead projector transparencies for a talk based on the paper Merging HOL with Set Theory are available as a single postscript file or as separate files for each transparency:
  1. TITLE: Merging HOL with Set Theory
  2. Type Theory is Popular
  3. Why is Type Theory Popular?
  4. Set Theory is More Standard
  5. Getting the Best of Both Worlds
  6. Overview of HOL
  7. Overview of HOL-ST
  8. ST: Set Theory in HOL
  9. Epsilon-operator and Axiom of Choice
  10. Auxiliary Notions
  11. Functions Inside ST
  12. Auxiliary Notions (1)
  13. Auxiliary Notions (2)
  14. Ordered Pairs and Products
  15. Relations and Functions
  16. Truthvalues and Numbers
  17. Experiment 1: lists of numbers
  18. Lists of numbers (details)
  19. Defining a HOL Type with List
  20. Lift Operations from ST to HOL
  21. Doesn't Work Polymorphically
  22. Transfer Principles
  23. Associating HOL Types with Sets
  24. Associating Constants with Sets
  25. Example Laws
  26. Interpreting HOL in ST
  27. HOL2ST
  28. Simplifying Transferred theorems
  29. Transferring Types
  30. Defining Types via ST
  31. Defining Constants via ST
  32. Polymorphic Lists
  33. Group Theory Example (QED)
  34. Groups in HOL
  35. Groups in ST
  36. Transferring HOL to ST
  37. Transferring Whole Theories
  38. HOL Abstract Theory of Groups
  39. Whole Theory Transferred to ST
  40. Conclusions and the Future