Independence results for calculi of dependent types | SpringerLink
Skip to main content
Springer Nature Link
Log in

Independence results for calculi of dependent types

  • Conference paper
  • First Online:
Category Theory and Computer Science

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

Abstract

Based on a categorical semantics for impredicative calculi of dependent types we prove several independence results. Especially we prove that there exists a model where all syntactical concepts can be interpreted with one exception: in the model the strong sum of a family of propositions indexed over a proposition need not be a proposition again. The method of proof consists of restricting the set of propositions in the well-known ω-Set model due to E. Moggi.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Hyland, A. Pitts The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models preprint, to appear in the Proceedings of the Conference on Categories in Computer Science and Logic, Contemporary Mathematics, Amer. Math.Soc., 1988.

    Google Scholar 

  2. J. Meseguer Universe Models and Initial Model Semantics for the Second Order Polymorphic Lambda Calculus abstract in “Abstracts of papers presented to A.M.S.”, Issue 58, Vol. 9, Num. 4, 1988.

    Google Scholar 

  3. A. Pitts Polymorphism is Set-Theoretic, Constructively Proc.of the Conference on Category Theory and Computer Science, Edinburgh 1987, SLNCS 283, 1987.

    Google Scholar 

  4. R. Seely Locally Cartesian Closed Categories and Type Theory. In Math.Proc. Cambridge Phil. Soc. 95, 1984.

    Google Scholar 

  5. R. Seely Categorical Semantics for Higher Order Polymorphic Lambda Calculus Journal of Symbolic Logic, 1987.

    Google Scholar 

  6. T. Streicher Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions Ph.D. Thesis, Univ. of Passau, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Mathematik und Informatik, Univ. Passau, D-8390, West Germany

    Thomas Streicher

Authors
  1. Thomas Streicher
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

David H. Pitt David E. Rydeheard Peter Dybjer Andrew M. Pitts Axel Poigné

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Streicher, T. (1989). Independence results for calculi of dependent types. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds) Category Theory and Computer Science. Lecture Notes in Computer Science, vol 389. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0018350

Download citation

  • DOI: https://doi.org/10.1007/BFb0018350

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51662-0

  • Online ISBN: 978-3-540-46740-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation