We show how PVS-style predicate subtyping can be simulated in HOL using predicate sets,a nd explain how to perform subtype checking using this model. We illustrate some applications of this to specification and verification in HOL,an d also demonstrate some limits of the approach. Finally we report on the effectiveness of a subtype checker used as a condition prover in a contextual rewriter.
CITATION STYLE
Hurd, J. (2001). Predicate Subtyping with predicate sets. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 265–280). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_19
Mendeley helps you to discover research relevant for your work.