research-article

Open access

The CtCoq System: Design and Architecture

Author:

Yves BertotAuthors Info & Claims

Formal Aspects of Computing, Volume 11, Issue 3

Pages 225 - 243

https://doi.org/10.1007/s001650050049

Published: 01 September 1999 Publication History

PDF eReader

Abstract.

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.

Cited By

View all

Gallego Arias EPin BJouvelot P(2017)jsCoq: Towards Hybrid Theorem Proving InterfacesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.239.2239(15-27)Online publication date: 24-Jan-2017
https://doi.org/10.4204/EPTCS.239.2
van der Hoeven JLecerf GRaux D(2017)Preserving Syntactic Correctness While Editing Mathematical FormulasApplications of Computer Algebra10.1007/978-3-319-56932-1_29(459-471)Online publication date: 27-Jul-2017
https://doi.org/10.1007/978-3-319-56932-1_29
Roe KSmith S(2016)CoqPIE: An IDE Aimed at Improving Proof Development ProductivityInteractive Theorem Proving10.1007/978-3-319-43144-4_32(491-499)Online publication date: 7-Aug-2016
https://doi.org/10.1007/978-3-319-43144-4_32
Show More Cited By

Index Terms

The CtCoq System: Design and Architecture

Index terms have been assigned to the content through auto-classification.

Recommendations

A user interface management system architecture for supporting separation of concerns and extensibility
A Graphical Specification System for User-Interface Design

An environment for creating user interfaces for embedded systems, called the graphical specification system (GSS), is presented. GSS combines graphical and minimal low-level textual specification with a prototyping capability for rapid user-interface ...
Reconciling usability and interactive system architecture using patterns

Traditional interactive system architectures such as MVC [Goldberg, A., 1984. Smaltalk-80: The Interactive Programming Environment, Addison-Wesley Publ.] and PAC [Coutaz, J., 1987. PAC, an implementation model for dialog design. In: Interact'87, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 11, Issue 3

Sep 1999

135 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 September 1999

Published in FAC Volume 11, Issue 3

Author Tag

Keywords: Interactive proof development; Graphical user interfaces; CtCoq; Proof by pointing; Proof maintenance

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
33
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)4

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Gallego Arias EPin BJouvelot P(2017)jsCoq: Towards Hybrid Theorem Proving InterfacesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.239.2239(15-27)Online publication date: 24-Jan-2017
https://doi.org/10.4204/EPTCS.239.2
van der Hoeven JLecerf GRaux D(2017)Preserving Syntactic Correctness While Editing Mathematical FormulasApplications of Computer Algebra10.1007/978-3-319-56932-1_29(459-471)Online publication date: 27-Jul-2017
https://doi.org/10.1007/978-3-319-56932-1_29
Roe KSmith S(2016)CoqPIE: An IDE Aimed at Improving Proof Development ProductivityInteractive Theorem Proving10.1007/978-3-319-43144-4_32(491-499)Online publication date: 7-Aug-2016
https://doi.org/10.1007/978-3-319-43144-4_32
(2015)Towards semantic mathematical editingJournal of Symbolic Computation10.1016/j.jsc.2014.09.04071:C(1-46)Online publication date: 1-Nov-2015
https://dl.acm.org/doi/10.1016/j.jsc.2014.09.040
Chaudhuri K(2013)Subformula linking as an interaction methodProceedings of the 4th international conference on Interactive Theorem Proving10.1007/978-3-642-39634-2_28(386-401)Online publication date: 22-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39634-2_28
Gast H(2012)Engineering the Prover InterfaceElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2012.06.002285:C(3-16)Online publication date: 19-Sep-2012
https://dl.acm.org/doi/10.1016/j.entcs.2012.06.002
Asperti ARicciotti WSacerdoti Coen CTassi E(2011)The Matita Interactive Theorem ProverAutomated Deduction – CADE-2310.1007/978-3-642-22438-6_7(64-69)Online publication date: 2011
https://doi.org/10.1007/978-3-642-22438-6_7
Sacerdoti Coen C(2009)A User Interface for a Mathematical System that Allows Ambiguous FormulaeElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2008.12.098226(67-87)Online publication date: Jan-2009
https://doi.org/10.1016/j.entcs.2008.12.098
Coen CTassi EZacchiroli S(2007)Tinycals: Step by Step TacticalsElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2006.09.026174:2(125-142)Online publication date: May-2007
https://doi.org/10.1016/j.entcs.2006.09.026
Mulhern AFischer CLiblit B(2007)Tool Support for Proof EngineeringElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2006.09.023174:2(75-86)Online publication date: 1-May-2007
https://dl.acm.org/doi/10.1016/j.entcs.2006.09.023
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract.

Cited By

Index Terms

Recommendations

A user interface management system architecture for supporting separation of concerns and extensibility

A Graphical Specification System for User-Interface Design

Reconciling usability and interactive system architecture using patterns

Comments

Information

Published In

Publisher

Publication History

Author Tag

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations