Lecture Notes in Computer Science, Volume 1827.
From Recent Trends in Algebraic Development Techniques, WADT '99.
Edited by D. Bert, C. Choppy and P. D. Mosses.
Springer-Verlag, Toulouse, France.
September, 1999.
Pages 37–52.

PVS (Prototype Verification System) is a mechanized framework for formal specification and interactive proof development. The PVS specification language is based on higher-order logic enriched with features such as predicate subtypes, dependent types, recursive datatypes, and parametric theories. Subtyping is a central concept in the PVS type system. PVS admits the definition of subtypes corresponding to nonzero integers, prime numbers, injective maps, order-preserving maps, and even empty subtypes. We examine the principles underlying the PVS subtype mechanism and its implementation and use.

@INPROCEEDINGS{Shankar:WADT99,
    AUTHOR = {Natarajan Shankar and Sam Owre},
    TITLE = {Principles and Pragmatics of Subtyping in {PVS}},
    VOLUME = {1827},
    YEAR = {1999},
    PAGES = {37--52},
    MONTH = {sep},
    ADDRESS = {Toulouse, France},
    URL = {http://www.csl.sri.com/papers/wadt99/},
    SERIES = {Lecture Notes in Computer Science},
    BOOKTITLE = {Recent Trends in Algebraic Development Techniques, {WADT} '99},
    PUBLISHER = {Springer-Verlag},
    EDITOR = {{D.} Bert and {C.} Choppy and {P.} {D.} Mosses}
}

• wadt99.pdf
• wadt99.ps