ANU: The Australian National University
_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [Research] [Teaching] [Publications] [Software] [CV]
_____________________________________________________________________

Towards a Browsable Record of HOL Proofs

Reference

Jim Grundy and Thomas Långbacka. Towards a Browsable Record of HOL Proofs. Technical Report 7. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland. April 1996.

Abstract

This paper presents the motivations for and current stage of development of a tool for recording HOL proofs in a browsable format. The proofs recorded are window inference proofs produced using the TkWinHOL interface to the HOL window Library. The ultimate aim of the work is to help resolve the conflicting requirements for formality and readability in proof.

BibTeX

Here is a suitable BibTeX entry: 
  @TECHREPORT{Grundy:1996:TBR,
    author      = "Jim Grundy and Thomas L{\aa}ngbacka",
    title       = "Towards a Browsable Record of {HOL}
                   Proofs",
    institution = "Turku Centre for Computer Science",
    address     = "Lemmink{\"a}isenkatu 14A,
                   20520 Turku, Finland",
    month       = may,
    year        = 1996,
    type        = "Technical Report",
    number      = "7"}

Citations

If you liked this paper, then you might also like the following papers which cite it:

Where To Find it

You can down-load a copy of the report; or, if you would like a paper copy you should write to the first author. If you want to try to find a copy in a library, the following might be useful:
Title: Towards a Browsable Record of HOL Proofs
Author: Jim Grundy and Thomas Långbacka
Copyright: 1996
ISBN: 951-650-748-4
Series: TUCS Technical Reports
Volume: 7
ISSN: 1239-1891
Publisher: Turku Centre for Computer Science
Address: Lemminkäisenkatu 14A, 20520 Turku, Finland
_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [Research] [Teaching] [Publications] [Software] [CV]
_____________________________________________________________________
Feedback & Queries: Jim Grundy
Date Last Modified: Thu 11 Nov 1999
Universal Ressource Locator: file:/home/jgrundy/www//Publications/tucstr7.html