Note: this work has been superseded by the deep and shallow embedding of ITL in Isabelle/HOL.
PVS is an interactive environment, developed at SRI, for writing formal speciﬁcations and checking formal proofs. The speciﬁcation language used in PVS is a strongly typed higher order logic. The powerful interactive theorem prover/proof checker of PVS has a large set of basic deductive steps and the facility to combine these steps into proof strategies. PVS is implemented in Common Lisp –with ancillary functions provided in C, Tcl/TK and LaTeX– and uses GNU Emacs for its interface. PVS is freely available for IBM RS6000 machines as well as Sun Sparcs under license from SRI. See PVS homepage for more information.