[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Kripke Semantics for Martin-Löf’s Extensional Type Theory

  • Conference paper
Typed Lambda Calculi and Applications (TLCA 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5608))

Included in the following conference series:

Abstract

It is well-known that simple type theory is complete with respect to non-standard models. Completeness for standard models only holds when increasing the class of models, e.g., to cartesian closed categories. Similarly, dependent type theory is complete for locally cartesian closed categories. However, it is usually difficult to establish the coherence of interpretations of dependent type theory, i.e., to show that the interpretations of equal expressions are indeed equal. Several classes of models have been used to remedy this problem.

We contribute to this investigation by giving a semantics that is both coherent and sufficiently general for completeness while remaining relatively easy to compute with. Our models interpret types of Martin-Löf’s extensional dependent type theory as sets indexed over posets or, equivalently, as fibrations over posets. This semantics can be seen as a generalization to dependent type theory of the interpretation of intuitionistic first-order logic in Kripke models. This yields a simple coherent model theory with respect to which simple and dependent type theory are sound and complete.

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.

Similar content being viewed by others

References

  1. Allen, S.: A Non-Type-Theoretic Definition of Martin-Löf’s Types. In: Gries, D. (ed.) Proceedings of the Second Annual IEEE Symp. on Logic in Computer Science, LICS 1987, pp. 215–221. IEEE Computer Society Press, Los Alamitos (1987)

    Google Scholar 

  2. Awodey, S., Rabe, F.: Kripke Semantics for Martin-Löf’s Extensional Type Theory (2009), http://kwarc.info/frabe/Research/LamKrip.pdf

  3. Cartmell, J.: Generalized algebraic theories and contextual category. Annals of Pure and Applied Logic 32, 209–243 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  4. Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5(1), 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  5. Curien, P.: Alpha-Conversion, Conditions on Variables and Categorical Logic. Studia Logica 48(3), 319–360 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  6. Friedman, H.: Equality Between Functionals. In: Parikh, R. (ed.) Logic Colloquium. LNMath, vol. 453, pp. 22–37. Springer, Heidelberg (1975)

    Chapter  Google Scholar 

  7. Henkin, L.: Completeness in the Theory of Types. Journal of Symbolic Logic 15(2), 81–91 (1950)

    Article  MathSciNet  MATH  Google Scholar 

  8. Hofmann, M.: On the Interpretation of Type Theory in Locally Cartesian Closed Categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 427–441. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  9. Hofmann, M.: Syntax and Semantics of Dependent Types. In: Pitts, A., Dybjer, P. (eds.) Semantics and Logic of Computation, pp. 79–130. Cambridge University Press, Cambridge (1997)

    Chapter  Google Scholar 

  10. Jacobs, B.: Categorical Type Theory. PhD thesis, Catholic University of the Netherlands (1990)

    Google Scholar 

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

    MATH  Google Scholar 

  12. Johnstone, P.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Science Publications (2002)

    Google Scholar 

  13. Kripke, S.: Semantical Analysis of Intuitionistic Logic I. In: Crossley, J., Dummett, M. (eds.) Formal Systems and Recursive Functions, pp. 92–130. North-Holland, Amsterdam (1965)

    Chapter  Google Scholar 

  14. Mac Lane, S.: Categories for the working mathematician. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  15. Lawvere, W.: Adjointness in Foundations. Dialectica 23(3–4), 281–296 (1969)

    Article  MATH  Google Scholar 

  16. Lipton, J.: Kripke Semantics for Dependent Type Theory and Realizability Interpretations. In: Myers, J., O’Donnell, M. (eds.) Constructivity in Computer Science, Summer Symposium, pp. 22–32. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  17. Mac Lane, S., Moerdijk, I.: Sheaves in geometry and logic. Lecture Notes in Mathematics. Springer, Heidelberg (1992)

    Book  MATH  Google Scholar 

  18. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)

    Google Scholar 

  19. Mitchell, J., Moggi, E.: Kripke-style Models for Typed Lambda Calculus. Annals of Pure and Applied Logic 51(1–2), 99–124 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  20. Mitchell, J., Scott, P.: Typed lambda calculus and cartesian closed categories. In: Categories in Computer Science and Logic. Contemporary Mathematics, vol. 92, pp. 301–316. Amer. Math. Society (1989)

    Google Scholar 

  21. Pitts, A.: Categorical Logic. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, ch. 2. Algebraic and Logical Structures, vol. 5, pp. 39–128. Oxford University Press, Oxford (2000)

    Google Scholar 

  22. Seely, R.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95, 33–48 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  23. Simpson, A.: Categorical completeness results for the simply-typed lambda-calculus. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) Typed Lambda Calculi and Applications, pp. 414–427 (1995)

    Google Scholar 

  24. Streicher, T.: Semantics of Type Theory. Springer, Heidelberg (1991)

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, Carnegie Mellon University, Pittsburgh, USA

    Steve Awodey

  2. School of Engineering and Science, Jacobs University Bremen, Germany

    Florian Rabe

Authors
  1. Steve Awodey
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Florian Rabe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire PPS (CNRS / Paris 7), Case 7014, Université Paris Diderot - Paris 7, 75205, Paris Cedex 13, France

    Pierre-Louis Curien

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Awodey, S., Rabe, F. (2009). Kripke Semantics for Martin-Löf’s Extensional Type Theory. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02273-9_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02272-2

  • Online ISBN: 978-3-642-02273-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics