{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:15Z","timestamp":1725474495778},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097794","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"216-235","source":"Crossref","is-referenced-by-count":1,"title":["The internal type theory of a Heyting pretopos"],"prefix":"10.1007","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"J. Adamek and J. Rosicky. Locally presentable and accessible categories., volume 189 of Lecture Notes Series. Cambridge University Press, 1994.","key":"12_CR1","DOI":"10.1017\/CBO9780511600579"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"10","DOI":"10.2307\/2273784","volume":"50","author":"J. Benabou","year":"1985","unstructured":"J. Benabou. Fibred categories and the foundations of naive category theory. Journal of Symbolic Logic, 50:10\u201337, 1985.","journal-title":"Journal of Symbolic Logic"},{"key":"12_CR3","first-page":"249","volume":"12","author":"A. Burroni","year":"1981","unstructured":"A. Burroni. Algebres graphiques. Cahiers de topologie et geometrie differentielle, 12:249\u2013265, 1981.","journal-title":"Cahiers de topologie et geometrie differentielle"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","unstructured":"J. Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209\u2013243, 1986.","journal-title":"Annals of Pure and Applied Logic"},{"unstructured":"R. Constable et al. Implementing mathematics with the Nuprl Development System. Prentice Hall, 1986.","key":"12_CR5"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"N.G. Bruijn de","year":"1991","unstructured":"N.G. de Bruijn. Telescopic mapping in typed lambda calculus. Information and Computation, 91:189\u2013204, 1991.","journal-title":"Information and Computation"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1016\/0021-8693(83)90197-7","volume":"81","author":"E.J. Dubuc","year":"1983","unstructured":"E.J. Dubuc and G. M. Kelly. A presentation of topoi as algebraic relative to categories and graphs. Journal of Algebra, 81:420\u2013433, 1983.","journal-title":"Journal of Algebra"},{"doi-asserted-by":"crossref","unstructured":"M. Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Proceedings of CSL'94, September 1994.","key":"12_CR8","DOI":"10.1007\/BFb0022273"},{"unstructured":"M. Hofmann. Extensional concept in intensional type theory. PhD thesis, University of Edinburgh, July 1995.","key":"12_CR9"},{"doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland and A. M. Pitts. The theory of constructions: Categorical semantics and topos theoretic models. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 137\u2013199, 1989.","key":"12_CR10","DOI":"10.1090\/conm\/092\/1003199"},{"unstructured":"B. Jacobs. Categorical type theory. PhD thesis, University of Nijmegen, 1991.","key":"12_CR11"},{"doi-asserted-by":"crossref","unstructured":"A. Joyal and I. Moerdijk. Algebraic set theory., volume 220 of Lecture Note Series. Cambridge University Press, 1995.","key":"12_CR12","DOI":"10.1017\/CBO9780511752483"},{"unstructured":"J. Lambek and P. J. Scott. An introduction to higher order categorical logic., volume 7 of Studies in Advanced Mathematics. Cambridge University Press, 1986.","key":"12_CR13"},{"unstructured":"M.E. Maietti. The typed theory of Heyting Pretopoi. Preprint-University of Padova, January 1997.","key":"12_CR14"},{"unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory, notes by G. Sambin of a series of lectures given in Padua. Bibliopolis, Naples, 1984.","key":"12_CR15"},{"unstructured":"S. MacLane and I. Moerdijk. Sheaves in Geometry and Logic. A first introduction to Topos Theory. Springer Verlag, 1992.","key":"12_CR16"},{"doi-asserted-by":"crossref","unstructured":"M. Makkai and G. Reyes. First order categorical logic., volume 611 of Lecture Notes in Mathematics. Springer Verlag, 1977.","key":"12_CR17","DOI":"10.1007\/BFb0066201"},{"key":"12_CR18","volume-title":"Programming in Martin L\u00f6f's Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Peterson, and J. Smith. Programming in Martin L\u00f6f's Type Theory. Clarendon Press, Oxford, 1990."},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/BF00370827","volume":"3","author":"A. Obtulowicz","year":"1989","unstructured":"A. Obtulowicz. Categorical and algebraic aspects of Martin L\u00f6f's type theory. Studia Logica, 3:299\u2013317, 1989.","journal-title":"Studia Logica"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R. Seely","year":"1984","unstructured":"R. Seely. Locally cartesian closed categories and type theory. Math. Proc. Cambr. Phyl. Soc., 95:33\u201348, 1984.","journal-title":"Math. Proc. Cambr. Phyl. Soc."},{"unstructured":"P. Taylor. Practical Foundations of Mathematics, volume 99 of Cambridge studies in advanced mathematics. Cambridge University Press, 1997.","key":"12_CR21"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097794","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T14:54:02Z","timestamp":1555944842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0097794","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}