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:
- TITLE: Merging HOL with Set Theory
- Type Theory is Popular
- Why is Type Theory Popular?
- Set Theory is More Standard
- Getting the Best of Both Worlds
- Overview of HOL
- Overview of HOL-ST
- ST: Set Theory in HOL
- Epsilon-operator and Axiom of Choice
- Auxiliary Notions
- Functions Inside ST
- Auxiliary Notions (1)
- Auxiliary Notions (2)
- Ordered Pairs and Products
- Relations and Functions
- Truthvalues and Numbers
- Experiment 1: lists of numbers
- Lists of numbers (details)
- Defining a HOL Type with List
- Lift Operations from ST to HOL
- Doesn't Work Polymorphically
- Transfer Principles
- Associating HOL Types with Sets
- Associating Constants with Sets
- Example Laws
- Interpreting HOL in ST
- HOL2ST
- Simplifying Transferred theorems
- Transferring Types
- Defining Types via ST
- Defining Constants via ST
- Polymorphic Lists
- Group Theory Example (QED)
- Groups in HOL
- Groups in ST
- Transferring HOL to ST
- Transferring Whole Theories
- HOL Abstract Theory of Groups
- Whole Theory Transferred to ST
- Conclusions and the Future