The CtCoq System: Design and Architecture.
In: Formal Aspects of Computing, Jg. 11 (1999-09-30), Heft 3, S. 225-243
Online
academicJournal
Zugriff:
The CtCoq user-interface is a graphical user-interface designed to be added to the Coq proof development system, acting as a broker between the human user and the logical engine. The principal design goal for CtCoq was to support large-scale proof development and we claim that this user-interface helps to increase the productivity of Coq users through powerful capabilities for elaborate mathematical notations, mouse interaction, and script management. In this paper, we review the user interface implementation to show how this design goal affects the capabilities provided by the system. [ABSTRACT FROM AUTHOR]
Copyright of Formal Aspects of Computing is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Titel: |
The CtCoq System: Design and Architecture.
|
---|---|
Autor/in / Beteiligte Person: | Bertot, Yves |
Link: | |
Zeitschrift: | Formal Aspects of Computing, Jg. 11 (1999-09-30), Heft 3, S. 225-243 |
Veröffentlichung: | 1999 |
Medientyp: | academicJournal |
ISSN: | 0934-5043 (print) |
DOI: | 10.1007/s001650050049 |
Sonstiges: |
|