An overview of the PVS system is presented from a user interface perspective. We present the interfaces from the PVS Lisp core to Emacs, Tcl/Tk, the Prover, markup languages, and some of the various back-end and front-end systems that have been integrated with PVS.
@inproceedings{PVSUI-UITP08,
AUTHOR = {Sam Owre},
TITLE = {A Brief Overview of the {PVS} User Interface},
BOOKTITLE = {8th International Workshop User Interfaces for
Theorem Provers (UITP'08)},
MONTH = aug,
YEAR = 2008,
ADDRESS = {Montreal, Canada},
NOTES = {Available at \url{http://www.ags.uni-sb.de/~omega/workshops/UITP08/UITP08-proceedings.pdf}}
}