Announcing PVS Version 2.3

We are pleased to announce the release of PVS 2.3.

PVS is a widely used theorem proving tool.  It is in roughly the same
class of systems as HOL, Nuprl, Isabelle, Coq, LEGO, etc.  It is a theorem
prover for a strongly typed higher-order logic based on Church's theory of
types.  It has a modern and novel type system based on predicate subtypes
and dependent types so that typechecking involves theorem proving.  A
fragment of the PVS language can also be used as an (extremely fast)
strongly typed functional language that exploits a number of type-based

Details are available at the PVS web site http://pvs.csl.sri.com

We hope you find PVS useful and fun,

The PVS Team