{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:33:16Z","timestamp":1784845996647,"version":"3.55.0"},"reference-count":30,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,9,27]],"date-time":"2011-09-27T00:00:00Z","timestamp":1317081600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>It is well-known that simple type theory is complete with respect to non-standard set-valued models. Completeness for standard models only holds with respect to certain extended classes of models, e.g., the class of 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 standard, coherent, and sufficiently general for completeness while remaining relatively easy to compute with. Our models interpret types of Martin-L\\\"of'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.<\/jats:p>","DOI":"10.2168\/lmcs-7(3:18)2011","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T13:45:24Z","timestamp":1415972724000},"source":"Crossref","is-referenced-by-count":3,"title":["Kripke Semantics for Martin-L\\\"of's Extensional Type Theory"],"prefix":"10.46298","volume":"Volume 7, Issue 3","author":[{"given":"Steve","family":"Awodey","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3040-3655","authenticated-orcid":false,"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2011,9,27]]},"reference":[{"key":"10.2168\/LMCS-7(3:18)2011_lcccallen","unstructured":"S. Allen. A Non-Type-Theoretic Definition of Martin-L\u00f6f's Types. In D. Gries, editor,Proceedings of the Second Annual IEEE Symp. on Logic in Computer Science, LICS 1987, pages 215-221. IEEE Computer Society Press, 1987."},{"key":"10.2168\/LMCS-7(3:18)2011_AR:lamkrip:09","doi-asserted-by":"crossref","unstructured":"S. Awodey and F. Rabe. Kripke Semantics for Martin-L\u00f6f's Extensional Type Theory. In P. Curien, editor,Typed Lambda Calculi and Applications (TLCA), volume 5608 ofLecture Notes in Computer Science, pages 249-263. Springer, 2009.","DOI":"10.1007\/978-3-642-02273-9_19"},{"key":"10.2168\/LMCS-7(3:18)2011_lambdacube","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors,Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"issue":"118","key":"10.2168\/LMCS-7(3:18)2011_spatialcover","first-page":"217","volume":"2","author":"C. Butz and I. Moerdijk","year":"1999","journal-title":"Compositio Mathematica"},{"key":"10.2168\/LMCS-7(3:18)2011_lccccartmell","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-7(3:18)2011_curry","unstructured":"H. Curry and R. Feys.Combinatory Logic. North-Holland, Amsterdam, 1958."},{"issue":"1","key":"10.2168\/LMCS-7(3:18)2011_churchtypes","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","journal-title":"Journal of Symbolic Logic"},{"issue":"3","key":"10.2168\/LMCS-7(3:18)2011_lccccurien","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00370828","volume":"48","author":"P. Curien","year":"1989","journal-title":"Studia Logica"},{"key":"10.2168\/LMCS-7(3:18)2011_friedman75equality","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0064870"},{"issue":"2","key":"10.2168\/LMCS-7(3:18)2011_henkintypes","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"10.2168\/LMCS-7(3:18)2011_lf","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper, F. Honsell, and G. Plotkin","year":"1993","journal-title":"Journal of the Association for Computing Machinery 40(1):143-184, 1993"},{"key":"10.2168\/LMCS-7(3:18)2011_lccchofmann","doi-asserted-by":"crossref","unstructured":"M. Hofmann. On the Interpretation of Type Theory in Locally Cartesian Closed Categories. InCSL, pages 427-441. Springer, 1994.","DOI":"10.1007\/BFb0022273"},{"key":"10.2168\/LMCS-7(3:18)2011_lccchofmann2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"10.2168\/LMCS-7(3:18)2011_howard","unstructured":"W. Howard. The formulas-as-types notion of construction. InTo H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 479-490. Academic Press, 1980."},{"key":"10.2168\/LMCS-7(3:18)2011_lcccjacobs","unstructured":"B. Jacobs.Categorical Type Theory. PhD thesis, Catholic University of the Netherlands, 1990."},{"key":"10.2168\/LMCS-7(3:18)2011_lcccjacobs2","unstructured":"B. Jacobs.Categorical Logic and Type Theory. Elsevier, 1999."},{"key":"10.2168\/LMCS-7(3:18)2011_johnstone","doi-asserted-by":"crossref","unstructured":"P. Johnstone.Sketches of an Elephant: A Topos Theory Compendium. Oxford Science Publications, 2002.","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"10.2168\/LMCS-7(3:18)2011_kripke65intuitionistic","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"issue":"3-4","key":"10.2168\/LMCS-7(3:18)2011_lawvereadjoint","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","volume":"23","author":"W. Lawvere","year":"1969","journal-title":"Dialectica"},{"key":"10.2168\/LMCS-7(3:18)2011_lccclipton","doi-asserted-by":"crossref","unstructured":"J. Lipton. Kripke Semantics for Dependent Type Theory and Realizability Interpretations. In J. Myers and M. O'Donnell, editors,Constructivity in Computer Science, Summer Symposium, pages 22-32. Springer, 1992.","DOI":"10.1007\/BFb0021080"},{"key":"10.2168\/LMCS-7(3:18)2011_categories","unstructured":"S. Mac Lane.Categories for the working mathematician. Springer, 1998."},{"key":"10.2168\/LMCS-7(3:18)2011_martinlofextensional","unstructured":"P. Martin-L\u00f6f.Intuitionistic Type Theory. Bibliopolis, 1984."},{"issue":"1-2","key":"10.2168\/LMCS-7(3:18)2011_mitchell91kripke","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0168-0072(91)90067-V","volume":"51","author":"J. Mitchell and E. Moggi","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-7(3:18)2011_sheaves","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"10.2168\/LMCS-7(3:18)2011_mitchell89lambdamodels","doi-asserted-by":"crossref","unstructured":"J. Mitchell and P. Scott. Typed lambda calculus and cartesian closed categories. InCategories in Computer Science and Logic, volume 92 ofContemporary Mathematics, pages 301-316. Amer. Math. Society, 1989.","DOI":"10.1090\/conm\/092\/1003204"},{"key":"10.2168\/LMCS-7(3:18)2011_pitts00catlog","doi-asserted-by":"crossref","unstructured":"A. Pitts. Categorical Logic. In S. Abramsky, D. Gabbay, and T. Maibaum, editors,Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, chapter 2, pages 39-128. Oxford University Press, 2000.","DOI":"10.1093\/oso\/9780198537816.003.0005"},{"key":"10.2168\/LMCS-7(3:18)2011_rabe:thesis:08","unstructured":"F. Rabe.Representing Logics and Logic Translations. PhD thesis, Jacobs University Bremen, 2008. see http:\/\/kwarc.info\/frabe\/Research\/phdthesis.pdf."},{"key":"10.2168\/LMCS-7(3:18)2011_lcccseely","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R. Seely","year":"1984","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"10.2168\/LMCS-7(3:18)2011_simpson95lambdamodels","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014068"},{"key":"10.2168\/LMCS-7(3:18)2011_lcccstreicher","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1184\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1184\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,5]],"date-time":"2024-06-05T00:35:27Z","timestamp":1717547727000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1184"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,27]]},"references-count":30,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(3:18)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1109.1702","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1109.1702","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9,27]]},"article-number":"1184"}}