PVS language is the result of a strong interaction between types and expressions, with the general paradigm:

    expression: type

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:

	expression constant | function | formula	type
declaration	c: typeexpr f(p1: typexpr1, ..., pn: typexprn): typexpr	t: TYPE t: TYPE+ t: TYPE FROM typexpr
definition	c: typeexpr = expr f(p1: typexpr1, ..., pn: typexprn): typexpr = expr	t: TYPE = typexpr
theorem	name: THEOREM formula

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:

• bad: PVS type checker is like a compiler that would not be able to automatically compile a program;
• good: TCC automatic generation help the user pinpoint specification flaws, and determine what needs to be proved;
• bad & good: the user has great freedom of expression and can write incorrect specifications, but won't be able to prove them correct.

Predicate subtyping, combined with dependant types, allows the specification of functions by means of types.

LAMBDA, EXISTS, FORALL uniform syntax

• (LAMBDA (x₁: typexpr₁, ..., x_n: typexpr_n): expr) with cosmetic variant {x₁: typexpr₁, ..., x_n: typexpr_n | expr} when expr: bool
• (EXISTS (x₁: typexpr₁, ..., x_n: typexpr_n): expr) when expr: bool
• (FORALL (x₁: typexpr₁, ..., x_n: typexpr_n): expr) when expr: bool

More on PVS language