A Comparative Study of Coq and HOL

Zammit, Vincent (1997) A Comparative Study of Coq and HOL. In: Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'97, Murray Hill, NJ, USA, 19/08/1997, Murray Hill NJ , ETATS-UNIS . (Full text available)

Download (190kB)
Download (225kB)


This paper illustrates the differences between the style of theory mechanisation of Coq and of HOL. This comparative study is based on the mechanisation of fragments of the theory of computation in these systems. Examples from these implementations are given to support some of the arguments discussed in this paper. The mechanisms for specifying definitions and for theorem proving are discussed separately, building in parallel two pictures of the different approaches of mechanisation given by these systems.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: interactive theorem proving, higher order logic, type thory
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 01 Aug 2009 14:30 UTC
Last Modified: 06 Sep 2011 03:55 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21466 (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year