# Papers on HOL and Set Theory

An invited talk
entitled * Higher Order Logic, Set Theory or Both?*, presented at
TPHOLs (Turku, Finland, August 1996)
**Abstract**

The majority of general purpose mechanised proof assistants
support versions of typed higher order logic, even though set theory
is the standard foundation for mathematics. For many applications
higher order logic works well and provides, for specification, the
benefits of type-checking that are well-known in programming. However,
there are areas where types get in the way or seem
unmotivated. Furthermore, most people with a scientific or engineering
background already know set theory, but not higher order logic. This
paper discusses some approaches to getting the best of both worlds: the
expressiveness and standardness of set theory with the efficient
treatment of functions provided by typed higher order logic.

Longer talk: [PDF].
Paper: [PDF].
A revised and extended version is also available
[PDF].

#### Earlier papers

@techreport{Gordon:HOLST94,

author = {M.J.C. Gordon},

title = {Merging HOL with Set Theory: preliminary experiments},

institution = {University of Cambridge Computer Laboratory},

number = {353},

year = 1994}

Available in postscript and dvi
forms. There is also a plain text
abstract and a colour postscript talk.

@techreport{Agerholm:Dinf94,

author = {S. Agerholm},

title = {Formalising a Model of the $\lambda$-calculus in {HOL-ST}},

institution = {University of Cambridge Computer Laboratory},

number = {354},

year = 1994}

Available in postscript
and dvi forms. There is also a
plain text abstract.

@techreport{AgerholmGordon,

author = {S. Agerholm and M.J.C. Gordon},

title = {Experiments with {ZF} {Set} {Theory} in {HOL} and {Isabelle}},

institution = {BRICS},

number = {RS-95-37},

year = 1995}

@inproceedings{Agerholm95experimentswith,

author = {Sten Agerholm and Mike Gordon},

title = {Experiments with ZF Set Theory in HOL and Isabelle},

booktitle = {in Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS},

year = {1995},

pages = {32--45},

publisher = {Springer-Verlag}
}

Cached at citeseer.

Sten Agerholm, Experiments in Formalizing Basic Category Theory in Higher Order Logic and Set Theory, 1995, unpublished draft.

**N.B.** these papers are primarily intended for readers
familiar with
HOL, but
others may find them interesting.