Principles and Pragmatics of Subtyping in PVS

1. Andrews, P.B.: An Introduction to Logic and Type Theory: To Truth through Proof. Academic Press, New York (1986)

   MATH  Google Scholar 

2. Barendregt, H.P.: The Lambda Calculus, its Syntax and Semantics. North-Holland, Amsterdam (1978)

   Google Scholar 

3. Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)

   Google Scholar 

4. Cardelli, L.: Type systems. In: Handbook of Computer Science and Engineering, ch. 103, pp. 2208–2236. CRC Press, Boca Raton (1997); Available at http://www.research.digital.com/SRC

   Google Scholar 

5. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Technical Report CDRL A005, Computer Science Laboratory, SRI International (March 1999)

   Google Scholar 

6. Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)

   Article  MathSciNet  MATH  Google Scholar 

7. Cheng, J.H., Jones, C.B.: On the usability of logics which handle partial functions. In: Morgan, C., Woodcock, J.C.P. (eds.) Proceedings of the Third Refinement Workshop, pp. 51–69. Springer, Heidelberg (1990)

   Google Scholar 

8. de Bruijn, N.G.: A survey of the project Automath. In: Curry, H.B. (ed.) Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 589–606. Academic Press, London (1980)

   Google Scholar 

9. Dowek, G., Felty, A., Herbelin, H., Huet, G., Paulin-Mohring, C., Werner, B.: The COQ proof assistant user’s guide: Version 5.6. Rapports Techniques 134, INRIA, Rocquencourt, France (December 1991)

   Google Scholar 

10. Futatsugi, K., Goguen, J., Jouanaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Reid, B.K. (ed.) 12th ACM Symposium on Principles of Programming Languages, pp. 52–66. Association for Computing Machinery (1985)

    Google Scholar 

11. Futatsugi, M., Goguen, J., Jouanaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Proceedings of the 12th ACM Symposium on Principles of Programming (1985)

    Google Scholar 

12. Frege, G.: Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought (1967); First published (1879)

    Google Scholar 

13. Frege, G.: Letter to Russell (1967); Written (1902)

    Google Scholar 

14. Griffioen, D., Huisman, M.: A comparison of PVS and Isabelle/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 123–142. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

15. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

16. Gordon, M.: Notes on PVS from a HOL perspective (August 1995), Available at http://www.cl.cam.ac.uk/users/mjcg/PVS.html

17. Jackson, P.: Undecidable typing, abstract theories and tactics in Nuprl and PVS (tutorial). In: von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)

    Google Scholar 

18. Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead (1990)

    MATH  Google Scholar 

19. Leveque, W.J.: Elementary Theory of Numbers. Dover, New York (1990); Originally published by Addison-Wesley (1962)

    MATH  Google Scholar 

20. Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Transactions on Programming Languages and Systems 21(3), 133–169 (1999)

    Article  Google Scholar 

21. Mosses, P.D.: Casl: A guided tour of its design. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol. 1589, pp. 216–240. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

22. Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)

    Article  Google Scholar 

23. Owre, S., Shankar, N.: Abstract datatypes in PVS. Technical Report SRI-CSL-93-9R, Computer Science Laboratory, SRI International, Menlo Park, CA (December 1993); Extensively revised (June 1997); Also available as NASA Contractor Report CR-97-206264

    Google Scholar 

24. Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA (August 1997)

    Google Scholar 

25. Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)

    MATH  Google Scholar 

26. Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering 24(9), 709–720 (1998)

    Article  Google Scholar 

27. Russell, B.: Letter to Frege (1967); Written (1902)

    Google Scholar 

28. Rushby, J.: Formal methods and the certification of critical systems. Technical Report SRI-CSL-93-7, Computer Science Laboratory, SRI International, Menlo Park, CA (December 1993); Also issued under the title Formal Methods and Digital Systems Validation for Airborne Systems as NASA Contractor Report 4551 (December 1993)

    Google Scholar 

29. Shankar, N.: Efficiently executing PVS. Project report, Computer Science Laboratory, SRI International, Menlo Park, CA (November 1999), Available at http://www.csl.sri.com/shankar/PVSeval.ps.gz

30. Spivey, J.M.: Understanding Z: A Specification Language and its Formal Semantics. Cambridge Tracts in Theoretical Computer Science 3. Cambridge University Press, Cambridge (1988)

    MATH  Google Scholar 

31. van Heijenoort, J. (ed.): From Frege to Gödel. Harvard University Press, Cambridge (1967)

    MATH  Google Scholar 

32. Whitehead, A.N., Russell, B.: Principia Mathematica, revised edition. Cambridge University Press, Cambridge (1925–1927); Three volumes. The first edition was published 1910–1913

    Google Scholar 

Download references