[Prev][Next][Index][Thread]
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
optimizations.
Details are available at the PVS web site http://pvs.csl.sri.com
We hope you find PVS useful and fun,
The PVS Team
pvs-bugs@csl.sri.com