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)
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.
- Depositors only (login required):