[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 
in PVS."
	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:

Kind regards,

Ken Kubota


Ken Kubota
doi: 10.4444/100