Skip to main content
SpringerLink
Log in

Subset Types and Partial Functions

  • Conference paper
Automated Deduction – CADE-19 (CADE 2003)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2741))

Included in the following conference series:

Abstract

A classical higher-order logic PFsub of partial functions is defined. The logic extends a version of Farmer’s logic PF by enriching the type system of the logic with subset types and dependent types. Validity in PFsub is then reduced to validity in PF by a translation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, P.: An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Academic Press, London (1965)

    Google Scholar 

  2. Andrews, P.: A Transfinite Type Theory with Type Variables. North-Holland, Amsterdam (1965)

    MATH  Google Scholar 

  3. Aspinall, D., Compagnoni, A.: Subtyping dependent types. Theoretical Computer Science 266(1-2) (2001)

    Google Scholar 

  4. Beeson, M.: Foundations of Constructive Mathematics: Metamathematical Studies. Springer, Heidelberg (1985)

    MATH  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  6. Coquand, T.: An analysis of Girard’s paradox. In: 1st Symposium on Logic in Computer Science, pp. 227–236 (1986)

    Google Scholar 

  7. Coquand, T.: A new paradox in type theory. In: 9th International Conference on Logic, Methodology, and Philosophy of Science, pp. 555–570 (1994)

    Google Scholar 

  8. Farmer, W.: A partial functions version of Church’s simple theory of types. The Journal of Symbolic Logic 55(3), 1269–1291 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  9. Farmer, W.: A simple type theory with partial functions and subtypes. Annals of Pure and Applied Logic 64(3) (1993)

    Google Scholar 

  10. Farmer, W., Guttman, J.: A Set Theory with Support for Partial Functions. Logica Studia 66(1), 59–78 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  11. Feferman, S.: Definedness. Erkenntnis 43, 295–320 (1995)

    Article  MathSciNet  Google Scholar 

  12. Girard, J.Y.: Une extension de l’interpretation de Gödel a l’analyse, et son application a l’elimination des coupures dans l’analyse et la theorie des types. In: 2nd Scandinavian Logic Symposium, pp. 63–92 (1971)

    Google Scholar 

  13. Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    MATH  MathSciNet  Google Scholar 

  14. Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)

    MATH  Google Scholar 

  15. Kerber, M., Kohlhase, M.: A Mechanization of Strong Kleene Logic for Partial Functions. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 371–385. Springer, Heidelberg (1994)

    Google Scholar 

  16. Kerber, M., Kohlhase, M.: Mechanising Partiality without Re-Implementation. In: Brewka, G., Habel, C., Nebel, B. (eds.) KI 1997. LNCS (LNAI), vol. 1303, pp. 123–134. Springer, Heidelberg (1997)

    Google Scholar 

  17. Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)

    Google Scholar 

  18. Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

  19. Owre, S., Shankar, N.: The formal semantics of PVS (March 1999), http://www.csl.sri.com/papers/csl-97-2/

  20. Pfenning, F.: Logical Frameworks. In: Robinson, A., Voronkov, A. (eds.) [21], ch. XXI, vol. 2 (2001)

    Google Scholar 

  21. Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier and MIT Press (2001)

    Google Scholar 

  22. 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 

  23. Stump, A.: Checking Validities and Proofs with CVC and flea. PhD thesis, Stanford University (2002), available from http://www.cs.wustl.edu/~stump/

  24. Stump, A.: Subset types and partial functions. draft paper available from author’s homepage (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science and Engineering, Washington University in St. Louis,  

    Aaron Stump

Authors
  1. Aaron Stump
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Theoretical Computer Science, TU Dresden, Germany

    Franz Baader

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Stump, A. (2003). Subset Types and Partial Functions. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45085-6_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40559-7

  • Online ISBN: 978-3-540-45085-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation