-
The CtCoq System: Design and Architecture
We present issues that arose in the design of the CtCoq user-interface for proof development. Covered issues include multi-processing, data display, mouse interaction,... -
Implementing Proof by Pointing without a Structure Editor
A proof by pointing user interface component allows a user to direct the course of a proof assistant by selecting terms with a mouse. Such a gesture is interpreted as... -
Subformula Linking as an Interaction Method
International audience
