Skip to main content

A Comparative Study of Coq and HOL

Zammit, Vincent (1997) A Comparative Study of Coq and HOL. In: Gunter, Elsa. L and Felty, Amy, eds. Theorem Proving in Higher Order Logics 10th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 323-337. ISBN 783540633792. E-ISBN 978-3-540-69526-4. (doi:10.1007/BFb0028403) (KAR id:21466)

Language: English
Download (190kB) Preview
Language: English
Download (225kB) Preview
Official URL


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: Book section
DOI/Identification number: 10.1007/BFb0028403
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: 31 May 2019 09:03 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year