A Reference Version of HOL

John Harrison and Konrad Slind.

Unpublished Supplementary Proceedings of the 1994 International Workshop on Higher Order Logic theorem proving and its applications, Valletta, Malta.

Abstract:

The second author has implemented a reference version of the HOL logic (henceforth called gtt). This version, written in Standard ML, is as simple as possible, making as few assumptions as necessary to present the essence of HOL. This simplicity makes the implementation easy to understand, to port, to develop, to change, and to informally reason about. The first author has ported gtt to another dialect of ML, and developed the parsing, prettyprinting, and typechecking support needed to take gtt beyond its initial rudimentary conception. The implementation of gtt has already been of use in developing a variant of the HOL logic.

DVI or PostScript

Bibtex entry

@UNPUBLISHED{harrison-slind,
        author          = "John Harrison and Konrad Slind",
        title           = "A Reference Version of {HOL}",
        note            = "Presented in poster session of 1994 HOL Users
                           Meeting and only published in participants'
                           supplementary proceedings. Available on the Web from
                  {\verb+http://www.dcs.glasgow.ac.uk/~hug94/sproc.html+}",
        year            = 1994}