An Open Source PVS4 with a Semantic User Interface

Supervisor       Dr Joseph Kiniry
Subject Area 	 Software Engineering
Pre-requisite 	 Very good knowledge of Common Lisp, Emacs, and compilers
Co-requisite 	 Deep knowledge of higher-order provers (PVS in
                 particular) and Emacs elisp programming will be
                 obtained during the course of this project 
Subject Coverage PVS, higher-order theorem provers, Common Lisp and
                 CLOS, Emacs and ELISP, Compiler Design and
                 Implementation
Project Type 	 Design & Implementation
Hardware 	 PC or workstation running x86/Linux, Mac OS X, or
                 SPARC/Solaris

Description
PVS is a higher-order theorem prover written in Allegro Common
Lisp. PVS's front-end is (X)Emacs. PVS was developed by the Formal
Methods and Dependable Systems Program in the Computer Science
Laboratory of SRI International, probably the leading formal methods
company in the world. SRI and is maintained by its primary author, Sam
Owre.

Allegro Common Lisp is one of the world's best IDEs. Unfortunately,
the runtime license for Allegro is quite expensive.

Recently, we convinced SRI to let us "port" PVS to an Open Source Lisp
implementation. Our target Open Source Lisp is CMUCL as it is broadly
available, has an active community, exhibits high performance, and is
99.9% ANSI-compliant. That port is already, for the most part,
finished for x86/Linux, though much debugging and testing remains. We
have only just begun trying to work in Mac OS X.

The UI of PVS is very rich and has many "bells and
whistles". Unfortunately, it was designed with a mathematician in
mind. Because provers like PVS are used by software professionals more
and more every day, we decided to add many of the features of modern
integrated development environments to PVS. As a result, we have
developed several new additions to the front-end using the CEDET
package for Emacs. These new features are called a "semantic user
interface" because they have been formalized in such a way as to
connect semantic constructs in the PVS language, higher-order logic,
and proof theory in a consistent fashion. The basic implementation of
this semantic UI is completed as well.

The goal of this project is to assist in completing the port of PVS to
CMUCL, finish the new semantic UI, and investigate new constructs and
UI idioms for interactive theorem provers.

Mandatory

1) Gain familiarity with PVS, Emacs, and CEDET.
2) Finish wisent PVS parser, integrating the PVS typechecker with the
wisent front-end.
3) Assist in the port and testing of PVS to CMUCL.
4) Implement the remaining features of the PVS semantic UI.
5) Investigate new constructs and UI idioms for interactive
higher-order provers.
6) Release a new version of PVS. Fame and fortune follow.

Discretionary

1) Help complete and test the port of CMUCL to Mac OS X.
2) Write, submit, and publish a paper on the results.

Exceptional

Help complete and test the port of CMUCL to AMD64/Linux and PPC/Linux.

Sources of information and preparatory reading

1) Emacs http://www.gnu.org/software/emacs/emacs.html
2) CEDET http://cedet.sourceforge.net/
3) Bison http://www.gnu.org/software/bison/bison.html
4) PVS http://pvs.csl.sri.com/
5) ICS http://www.icansolve.com/
6) Common Lisp http://www.lisp.org/
7) CMUCL http://www.cons.org/cmucl/
8) Read "Improving the PVS User Interface" available via
http://www.kindsoftware.com/~kiniry/papers_index.html
9) Email me (kiniry@acm.org) for a copy of "Formalizing the User's
Context to Support User Interfaces for Integrated Mathematical
Environments."