SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Principles and Pragmatics of Subtyping in PVS
 by Sam Owre & Dr. Natarajan Shankar.

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.
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 = {},
    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}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy