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)

Postscript
Download (190kB)
[img]
Preview
PDF
Download (225kB)
[img]
Preview

Abstract

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 > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 01 Aug 2009 14:30
Last Modified: 06 Sep 2011 03:55
Resource URI: http://kar.kent.ac.uk/id/eprint/21466 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year