Papers on HOL and Set Theory


An invited talk entitled Higher Order Logic, Set Theory or Both?, presented at TPHOLs (Turku, Finland, August 1996) 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.