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.
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}