Skip to main content
Kent Academic Repository

Proving as Programming with DrHOL: A Preliminary Design

Owens, Scott, Slind, Konrad (2003) Proving as Programming with DrHOL: A Preliminary Design. In: Technical report 189. . pp. 123-132. Institut für Informatik, Albert-Ludwigs-Universität Freiburg (KAR id:31921)


We discuss the design of a new implementation of the HOL system aimed at improved graphical user interface support for formal proof. We call our approach Proving as Programming, since we believe that metalanguage programming is a central aspect of proof construction. Thus we look to contemporary programming environments for inspiration on how to provide graphical support for proof. In particular, our implementation builds upon DrScheme, a popular programming environment for Scheme. 1 Proving as Programming We have begun work on DrHOL, a new implementation of the HOL logic. DrHOL is systematically derived from HOL-4 [8] and aims at improving user interfaces in many aspects of work in HOL: development of proof procedures, construction of terms and definitions, interactive proof, and embedding of object languages are seen as candidates for better interface support. We believe that programmability is an essential part of all these activities.

Item Type: Conference or workshop item (Paper)
Additional information: Technical report 189
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 05 Nov 2013 17:50 UTC
Last Modified: 16 Nov 2021 10:09 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.