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)
|
Postscript
Language: English |
|
|
Download this file (Postscript/190kB) |
Preview |
| Request a format suitable for use with assistive technology e.g. a screenreader | |
|
PDF
Language: English |
|
|
Download this file (PDF/225kB) |
Preview |
| Request a format suitable for use with assistive technology e.g. a screenreader | |
| Official URL: http://dx.doi.org/10.1007/BFb0028403 |
|
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: | 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: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 01 Aug 2009 14:30 UTC |
| Last Modified: | 16 Nov 2021 09:59 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/21466 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Altmetric
Altmetric
