Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Principles and Pragmatics of Subtyping in PVS

Presented at the 14th International Workshop on Algebraic Development Techniques (WADT'99)


Natarajan Shankar and Sam Owre


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.

gzipped postscript or postscript

BibTeX Entry

    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}
Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Wed 24 Nov 2010 14:08 PST
Maintainer: Sam Owre