PVS: Principles and Pragmatics Natarajan Shankar shankar@csl.sri.com SRI International Computer Science Laboratory Menlo Park, CA, USA

WADT'99

PVS is a mechanized framework for specification and verification. The PVS specification language is intended as an expressive medium for formalizing mathematical and computational discourse. The language is based on a higher-order logic enhanced with features such as predicate subtypes, dependent types, recursive datatypes, and parametric theories. This talk critically examines the principles and pragmatic considerations underlying the design of the PVS specification language. The design choices in PVS are compared with those in other similar specification languages. No prior knowledge of PVS is assumed in the talk.