Predicate Subtyping with Predicate Sets

1. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

   Article  MATH  MathSciNet  Google Scholar 

2. Adriana Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, Catholic University, Nigmegen, January 1995.

   Google Scholar 

3. M. J. C. Gordon. Notes on PVS from a HOL perspective. Available from the University of Cambridge Computer Laboratory web server.

   Google Scholar 

4. M. J. C. Gordon and T. F. Melham. Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, 1993.

   Google Scholar 

5. John Harrison. Optimizing proof search in model elimination. In M. A. McRobbie and J. K. Slaney, editors, 13th International Conference on Automated Deduction, volume 1104 of Lecture Notes in Computer Science, pages 313–327, New Brunswick, NJ, 1996. Springer-Verlag.

   Google Scholar 

6. Joe Hurd. Verification of the Miller-Rabin probabilistic primality test. Submitted as a Category B paper to TPHOLs 2001, May 2001.

   Google Scholar 

7. Michael D. Jones. Restricted types for HOL. In TPHOLs 1997 Category B papers, 1997.

   Google Scholar 

8. Matt Kaufmann and J. S. Moore. Industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203–213, April 1997.

   Google Scholar 

9. Leslie Lamport and Lawrence C. Paulson. Should your specification language be typed? ACM Transactions on Programming Languages and Systems, 21(3):502–526, May 1999.

   Google Scholar 

10. Harry G. Mairson. Deciding ML typability is complete for deterministic exponential time. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 382–401. ACM SIGACT and SIGPLAN, ACM Press, 1990.

    Google Scholar 

11. R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, December 1978.

    Google Scholar 

12. Abdel Mokkedem and Tim Leonard. Formal verification of the Alpha 21364 network protocol. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 443–461, Portland, OR, August 2000. Springer-Verlag.

    Chapter  Google Scholar 

13. S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS System Guide. Computer Science Laboratory, SRI International, Menlo Park, CA, September 1999.

    Google Scholar 

14. Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA, August 1997.

    Google Scholar 

15. J. A. Robinson. A note on mechanizing higher order logic. Machine Intelligence, 5:121–135, 1970.

    Google Scholar 

16. Mark Saaltink. Domain checking Z specifications. In C. Michael Holloway and Kelly J. Hayhurst, editors, LFM’ 97: Fourth NASA Langley Formal Methods Workshop, pages 185–192, Hampton, VA, September 1997.

    Google Scholar 

17. Natarajan Shankar and Sam Owre. Principles and pragmatics of subtyping in PVS. In D. Bert, C. Choppy, and P. D. Mosses, editors, Recent Trends in Algebraic Development Techniques, WADT’ 99, volume 1827 of Lecture Notes in Computer Science, pages 37–52, Toulouse, France, September 1999. Springer-Verlag.

    Google Scholar 

18. Wai Wong. The HOL res_quan library. HOL88 documentation.

    Google Scholar 

Download references