{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:49:53Z","timestamp":1743115793231,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642022722"},{"type":"electronic","value":"9783642022739"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02273-9_19","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T14:12:17Z","timestamp":1246025537000},"page":"249-263","source":"Crossref","is-referenced-by-count":3,"title":["Kripke Semantics for Martin-L\u00f6f\u2019s Extensional Type Theory"],"prefix":"10.1007","author":[{"given":"Steve","family":"Awodey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","first-page":"215","volume-title":"Proceedings of the Second Annual IEEE Symp. on Logic in Computer Science, LICS 1987","author":"S. Allen","year":"1987","unstructured":"Allen, S.: A Non-Type-Theoretic Definition of Martin-L\u00f6f\u2019s Types. In: Gries, D. (ed.) Proceedings of the Second Annual IEEE Symp. on Logic in Computer Science, LICS 1987, pp. 215\u2013221. IEEE Computer Society Press, Los Alamitos (1987)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Awodey, S., Rabe, F.: Kripke Semantics for Martin-L\u00f6f\u2019s Extensional Type Theory (2009), http:\/\/kwarc.info\/frabe\/Research\/LamKrip.pdf","DOI":"10.1007\/978-3-642-02273-9_19"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","unstructured":"Cartmell, J.: Generalized algebraic theories and contextual category. Annals of Pure and Applied Logic\u00a032, 209\u2013243 (1986)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"19_CR4","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic\u00a05(1), 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"issue":"3","key":"19_CR5","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00370828","volume":"48","author":"P. Curien","year":"1989","unstructured":"Curien, P.: Alpha-Conversion, Conditions on Variables and Categorical Logic. Studia Logica\u00a048(3), 319\u2013360 (1989)","journal-title":"Studia Logica"},{"key":"19_CR6","series-title":"LNMath","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/BFb0064870","volume-title":"Logic Colloquium","author":"H. Friedman","year":"1975","unstructured":"Friedman, H.: Equality Between Functionals. In: Parikh, R. (ed.) Logic Colloquium. LNMath, vol.\u00a0453, pp. 22\u201337. Springer, Heidelberg (1975)"},{"issue":"2","key":"19_CR7","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the Theory of Types. Journal of Symbolic Logic\u00a015(2), 81\u201391 (1950)","journal-title":"Journal of Symbolic Logic"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BFb0022273","volume-title":"Computer Science Logic","author":"M. Hofmann","year":"1995","unstructured":"Hofmann, M.: On the Interpretation of Type Theory in Locally Cartesian Closed Categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, pp. 427\u2013441. Springer, Heidelberg (1995)"},{"key":"19_CR9","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1017\/CBO9780511526619.004","volume-title":"Semantics and Logic of Computation","author":"M. Hofmann","year":"1997","unstructured":"Hofmann, M.: Syntax and Semantics of Dependent Types. In: Pitts, A., Dybjer, P. (eds.) Semantics and Logic of Computation, pp. 79\u2013130. Cambridge University Press, Cambridge (1997)"},{"key":"19_CR10","unstructured":"Jacobs, B.: Categorical Type Theory. PhD thesis, Catholic University of the Netherlands (1990)"},{"key":"19_CR11","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Johnstone, P.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Science Publications (2002)","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/S0049-237X(08)71685-9","volume-title":"Formal Systems and Recursive Functions","author":"S. Kripke","year":"1965","unstructured":"Kripke, S.: Semantical Analysis of Intuitionistic Logic I. In: Crossley, J., Dummett, M. (eds.) Formal Systems and Recursive Functions, pp. 92\u2013130. North-Holland, Amsterdam (1965)"},{"key":"19_CR14","volume-title":"Categories for the working mathematician","author":"S. Mac Lane","year":"1998","unstructured":"Mac Lane, S.: Categories for the working mathematician. Springer, Heidelberg (1998)"},{"issue":"3\u20134","key":"19_CR15","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","volume":"23","author":"W. Lawvere","year":"1969","unstructured":"Lawvere, W.: Adjointness in Foundations. Dialectica\u00a023(3\u20134), 281\u2013296 (1969)","journal-title":"Dialectica"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/BFb0021080","volume-title":"Constructivity in Computer Science, Summer Symposium","author":"J. Lipton","year":"1992","unstructured":"Lipton, J.: Kripke Semantics for Dependent Type Theory and Realizability Interpretations. In: Myers, J., O\u2019Donnell, M. (eds.) Constructivity in Computer Science, Summer Symposium, pp. 22\u201332. Springer, Heidelberg (1992)"},{"key":"19_CR17","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0","volume-title":"Sheaves in geometry and logic","author":"S. Mac Lane","year":"1992","unstructured":"Mac Lane, S., Moerdijk, I.: Sheaves in geometry and logic. Lecture Notes in Mathematics. Springer, Heidelberg (1992)"},{"key":"19_CR18","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"issue":"1\u20132","key":"19_CR19","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0168-0072(91)90067-V","volume":"51","author":"J. Mitchell","year":"1991","unstructured":"Mitchell, J., Moggi, E.: Kripke-style Models for Typed Lambda Calculus. Annals of Pure and Applied Logic\u00a051(1\u20132), 99\u2013124 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Mitchell, J., Scott, P.: Typed lambda calculus and cartesian closed categories. In: Categories in Computer Science and Logic. Contemporary Mathematics, vol.\u00a092, pp. 301\u2013316. Amer. Math. Society (1989)","DOI":"10.1090\/conm\/092\/1003204"},{"key":"19_CR21","series-title":"Algebraic and Logical Structures","first-page":"39","volume-title":"Handbook of Logic in Computer Science, ch. 2","author":"A. Pitts","year":"2000","unstructured":"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.\u00a05, pp. 39\u2013128. Oxford University Press, Oxford (2000)"},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R. Seely","year":"1984","unstructured":"Seely, R.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc.\u00a095, 33\u201348 (1984)","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013427 (1995)","DOI":"10.1007\/BFb0014068"},{"key":"19_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6","volume-title":"Semantics of Type Theory","author":"T. Streicher","year":"1991","unstructured":"Streicher, T.: Semantics of Type Theory. Springer, Heidelberg (1991)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02273-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,14]],"date-time":"2024-03-14T22:03:38Z","timestamp":1710453818000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02273-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642022722","9783642022739"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02273-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}