Formalizing the User's Context to Support User Interfaces for Integrated Mathematical Environments
Joseph R. Kiniry · Electronic Notes in Theoretical Computer Science · 2004
This paper describes the several user-interface features for interactive theorem provers.Many of these features mimic functionality that already exists, and have great utility, in modern interactive development environments (IDEs).A formal kind theoretic model of a user's context is also presented.This model is used to formally describe the structure, behavior, and customization of the features.The functionality presented include browsers for basic mathematical constructs (declarations, theories, types, proofs, etc.), quick access to constructs definitions and uses (a short-cut sidebar, menus, or implicit hyperlinks), built-in contextual help, context-and type-aware completion and visual representation (expanding and collapsing structured elements of specifications, proof terms, and sequents), the graphical representation of language elements, and a user-extensible, type-aware pretty-printer.Research opportunities in interface design based upon the formal model are also identified and discussed.These features have been added to the PVS theorem prover as a proof-of-concept and will be available in its next major release.