Concepedia

Subtypes for specifications: predicate subtyping in PVS

John Rushby, Sam Owre, Natarajan Shankar

IEEE Transactions on Software Engineering · 1998 · 139 citations · 16 references

DOI

Concepts

Abstract

A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called "predicate subtyping" that uses this capability and illustrate its utility as mechanized in PVS.

References

16

A formulation of the simple theory of types

Alonzo Church · Journal of Symbolic Logic · 1940 · 1.9K citations

, , +9

Systematic software development using VDM

Sunil Vadera · Data Processing · 1986 · 1.1K citations

, , +11

Mathematical Logic as Based on the Theory of Types

Bertrand Russell · American Journal of Mathematics · 1908 · 938 citations

, , +11

Formal verification for fault-tolerant architectures: prolegomena to the design of PVS

Sam Owre, John Rushby, Natarajan Shankar et al. · IEEE Transactions on Software Engineering · 1995 · 494 citations

, , +15

Bertrand Russell. Mathematical logic as based on the theory of types. A reprint of the first five sections of 111<i>16</i>. Contemporary readings in logical theory, edited by Irving M. Copi and James A. Gould, The Macmillan Company, New York, and Collier-Macmillan Limited, London, 1967, pp. 135–153.

Alonzo Church · Journal of Symbolic Logic · 1974 · 484 citations

, , +15