PVS language is the result of a strong interaction between types and expressions, with the general paradigm:
A PVS theory is essentially a list of declarations or definitions of expressions or types, plus theorems. There are thus two dimensions in this language:
Function declaration or definition is a cosmetic variant of constant declaration or definition: it does not add any expressive power.
PVS type language is so powerful, because of subtyping (by means of predicates) that type checking is undecidable: this is why PVS generates TCCs (Type Checking Conditions) that often require user interaction (to come up with proofs). Undecidability of type checking can be viewed as a bad and good thing:
Predicate subtyping, combined with dependant types, allows the specification of functions by means of types.
LAMBDA, EXISTS, FORALL uniform syntax
The presentation below has been converted from “PowerPoint” to “Google Slides” format: please note that the conversion is not perfect, wait for fixes. Go to bottom of the page for “ppt” or “pdf” versions.