Papers on HOL and Set Theory

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.

Paper: [postscript | dvi]. A revised and extended version is also available [postscript].

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}

Available from BRICS via anonymous FTP (in directory pub/BRICS).

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