Skip to main content
SpringerLink
Log in

Collection Principles in Dependent Type Theory

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2277))

Included in the following conference series:

Abstract

We introduce logic-enriched intuitionistic type theories, that extend intuitionistic dependent type theories with primitive judgements to express logic. By adding type theoretic rules that correspond to the collection axiom schemes of the constructive set theory CZF we obtain a generalisation of the type theoretic interpretation of CZF. Suitable logic-enriched type theories allow also the study of reinterpretations of logic. We end the paper with an application to the double-negation interpretation.

This paper was written while visiting the Mittag-Leffler Institute, The Royal Swedish Academy of Sciences. Both authors wish to express their gratitude for the invitation to visit the Institute. The first author is also grateful to his two departments for supporting his visit. The second author is grateful to his department and to the “Fondazione Ing. A. Gini” for supporting his visit.

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. Peter Aczel, The Type Theoretic Interpretation of Constructive Set TheoryA. MacIntyre, L. Pacholski and J. Paris (eds.), Logic Colloquium’77, (North-Holland, Amsterdam, 1978).

    Google Scholar 

  2. Peter Aczel, The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions, R.B. Barcan Marcus, G. J. W. Dorn and P. Weingartner (eds.) Logic, Methodology and Philosophy of Science, VII, (North-Holland, Amsterdam, 1986).

    Google Scholar 

  3. Peter Aczel, Notes on Constructive Set Theory, Draft manuscript. Available at http://www.cs.man.ac.uk/~petera, 1997.

  4. Peter Aczel, On Relating Type Theories and Set Theories, in T. Altenkirch, W. Naraschewski and B. Reus (eds.) Types for Proofs and Programs, Proceedings of Types’98, LNCS 1657, (1999).

    Google Scholar 

  5. Peter Aczel, The Russell-Prawitz Modality, Mathematical Structures in Computer Science, vol. 11, (2001) 1–14.

    Article  Google Scholar 

  6. Peter Aczel and Michael Rathjen, Notes on Constructive Set Theory, Preprint no. 40, Institut Mittag-Leffer, The Royal Swedish Academy of Sciences, 2001. Available at http://www.ml.kva.se.

  7. Thierry Coquand and Erik Palmgren, Intuitionistic Choice and Classical Logic, Archive for Mathematical Logic, vol. 39 (2000) 53–74.

    Article  MATH  MathSciNet  Google Scholar 

  8. Thierry Coquand, Giovanni Sambin, Jan Smith and Silvio Valentini, Inductively Generated Formal Topologies, Submitted for publication, 2000.

    Google Scholar 

  9. Harvey M. Friedman, The Consistency of Classical Set Theory Relative to a Set Theory with Intuitionistic Logic, Journal of Symbolic Logic, vol. 38 (1973) 315–319.

    Article  MATH  MathSciNet  Google Scholar 

  10. Nicola Gambino and Peter Aczel, Frame-Valued Semantics for Constructive Set Theory, Preprint no. 39, Institut Mittag-Leffer, The Swedish Royal Academy of Sciences, 2001. Available at http://www.ml.kva.se.

  11. Robin Grayson, Forcing in Intuitionistic Theories without Power Set, Journal of Symbolic Logic, vol. 48 (1983) 670–682.

    Article  MATH  MathSciNet  Google Scholar 

  12. Robin Grayson, Heyting-valued models for Intuitionistic Set Theory, in M. Fourman, C. Mulvey and D.S. Scott (eds.) Applications of Sheaves, vol. 743, SLNM (1979).

    Google Scholar 

  13. Edward Griffor and Michael Rathjen, The Strength of Some Martin-Löf’s Type Theories, Archiv for Mathematical Logic vol. 33, (1994) 347–385.

    Article  MATH  MathSciNet  Google Scholar 

  14. Peter T. Johnstone, Stone Spaces, (Cambridge University Press, Cambridge, 1982).

    MATH  Google Scholar 

  15. Per Martin-Löf, Intuitionistic Type Theories, (Bibliopolis, Napoli, 1984).

    Google Scholar 

  16. Saunders MacLane and Ieke Moerdijk, Sheaves in Geometry and Logic. A First Introduction to Topos Theory, (Springer, Berlin, 1992).

    Google Scholar 

  17. Ieke Moerdijk and Erik Palmgren, Wellfounded Trees in Categories, Annals of Pure and Applied Logic, vol. 104, (2000) 189–218.

    Article  MATH  MathSciNet  Google Scholar 

  18. Ieke Moerdijk and Erik Palmgren, Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST, Annals of Pure and Applied Logic, to appear.

    Google Scholar 

  19. Michael Rathjen, Edward Griffor and Erik Palmgren, Inaccessibility in Constructive Set Theory and Type Theory, Annals of Pure and Applied Logic, vol. 94, (1998) 181–200.

    Article  MATH  MathSciNet  Google Scholar 

  20. Giovanni Sambin, Intuitionistic Formal Spaces, in D. Skordev (ed.) Mathematical Logic and its Applications (Plenum, New York, 1987), 187–204.

    Google Scholar 

  21. Anne Troelstra and Dirk van Dalen, Constructivism in Mathematics, Vol. 1, Studies in Logic No. 121, (North Holland, 1988).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departments of Mathematics and Computer Science, University of Manchester, Manchester

    Peter Aczel

  2. Department of Computer Science, University of Manchester, Manchester

    Nicola Gambino

Authors
  1. Peter Aczel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicola Gambino
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK

    Paul Callaghan , Zhaohui Luo , James McKinna  & Robert Pollack , ,  & 

  2. Division of Informatics Laboratory for Foundations of Computer Science, The University of Edinburgh, James Clerk Maxwell Building, The King’s Buildings Mayfield Road, EH9 3JZ, Edinburgh, Scotland, UK

    Robert Pollack

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aczel, P., Gambino, N. (2002). Collection Principles in Dependent Type Theory. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds) Types for Proofs and Programs. TYPES 2000. Lecture Notes in Computer Science, vol 2277. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45842-5_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-45842-5_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43287-6

  • Online ISBN: 978-3-540-45842-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation