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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Awodey, S., Rabe, F.: Kripke Semantics for Martin-Löf’s Extensional Type Theory (2009), http://kwarc.info/frabe/Research/LamKrip.pdf
Cartmell, J.: Generalized algebraic theories and contextual category. Annals of Pure and Applied Logic 32, 209–243 (1986)
Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5(1), 56–68 (1940)
Curien, P.: Alpha-Conversion, Conditions on Variables and Categorical Logic. Studia Logica 48(3), 319–360 (1989)
Friedman, H.: Equality Between Functionals. In: Parikh, R. (ed.) Logic Colloquium. LNMath, vol. 453, pp. 22–37. Springer, Heidelberg (1975)
Henkin, L.: Completeness in the Theory of Types. Journal of Symbolic Logic 15(2), 81–91 (1950)
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)
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)
Jacobs, B.: Categorical Type Theory. PhD thesis, Catholic University of the Netherlands (1990)
Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)
Johnstone, P.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Science Publications (2002)
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)
Mac Lane, S.: Categories for the working mathematician. Springer, Heidelberg (1998)
Lawvere, W.: Adjointness in Foundations. Dialectica 23(3–4), 281–296 (1969)
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)
Mac Lane, S., Moerdijk, I.: Sheaves in geometry and logic. Lecture Notes in Mathematics. Springer, Heidelberg (1992)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
Mitchell, J., Moggi, E.: Kripke-style Models for Typed Lambda Calculus. Annals of Pure and Applied Logic 51(1–2), 99–124 (1991)
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)
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)
Seely, R.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95, 33–48 (1984)
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)
Streicher, T.: Semantics of Type Theory. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)