School of Computing

A comparative study of Coq and HOL

Vincent Zammit

In Elsa L. Gunter and Amy Felty, editors, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'97, Murray Hill, NJ, USA, volume 1275 of Lecture Notes in Computer Science, pages 182-196. Springer, August 1997.

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.

Download publication 185 kbytes (PostScript)

Bibtex Record

@inproceedings{394,
author = {Vincent Zammit},
title = {A Comparative Study of {C}oq and {H}{O}{L}},
month = {August},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/394},
    ISBN = {3-540-63379-0},
    ISSN = {0302-9743},
    booktitle = {Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'97, Murray Hill, NJ, USA},
    editor = {Elsa L. Gunter and Amy Felty},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    volume = {1275},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014