[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Dependent types in PVS
Dear PVS Users and Developers,
According to the 1999 paper (published in 2000) by Sam Owre and Natarajan
Shankar "[i]n PVS, the dependencies can only affect the predicates in a type
but not its structure. For example, the type [n : nat -> A^n] cannot be defined
http://www.csl.sri.com/papers/wadt99/wadt99.pdf (p. 13, see also p. 9)
This would mean that some mappings from terms to types, e.g., 3 -> R^3
(= R x R x R), could not be expressed. Is this still valid as of today (2016)?
The PVS Language Reference (Version 2.4, November 2001) available at
doesn't provide any other information in section 4.5 (Dependent types).
The background of my question is a classification of current logics and
implementations by their expressiveness in terms of the syntactic features of
the formal language: