{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:21Z","timestamp":1776316941368,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600176","type":"print"},{"value":"9783540494041","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0022273","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T01:12:29Z","timestamp":1132621949000},"page":"427-441","source":"Crossref","is-referenced-by-count":45,"title":["On the interpretation of type theory in locally cartesian closed categories"],"prefix":"10.1007","author":[{"given":"Martin","family":"Hofmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"31_CR1","unstructured":"Michael Barr and Charles Wells. Category Theory for Computing Science. International Series in Computer Science. Prentice Hall, 1990."},{"key":"31_CR2","doi-asserted-by":"crossref","first-page":"10","DOI":"10.2307\/2273784","volume":"50","author":"J. B\u00e9nabou","year":"1985","unstructured":"J. B\u00e9nabou. Fibred categories and the foundations of naive category theory. Journal of Symbolic Logic, 50:10\u201337, 1985.","journal-title":"Journal of Symbolic Logic"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"A. Carboni. Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra, to appear.","DOI":"10.1016\/0022-4049(94)00103-P"},{"key":"31_CR4","unstructured":"J. Cartmell. Generalized algebraic theories and contextual categories. PhD thesis, Univ. Oxford, 1978."},{"key":"31_CR5","doi-asserted-by":"crossref","first-page":"51","DOI":"10.3233\/FI-1993-191-204","volume":"19","author":"P. Curien","year":"1993","unstructured":"Pierre-Louis Curien. Substitution up to isomorphism. Fundamenta Informaticae, 19:51\u201386, 1993.","journal-title":"Fundamenta Informaticae"},{"key":"31_CR6","first-page":"213","volume-title":"LNCS vol. 389","author":"T. Ehrhard","year":"1989","unstructured":"Thomas Ehrhard. Dictoses. In Proc. Conf. Category Theory and Computer Science, Manchester, UK, pages 213\u2013223. Springer LNCS vol. 389, 1989."},{"key":"31_CR7","unstructured":"Bart Jacobs. Categorical Type Theory. PhD thesis, University of Nijmegen, 1991."},{"key":"31_CR8","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(93)90169-T","volume":"107","author":"B. Jacobs","year":"1993","unstructured":"Bart Jacobs. Comprehension categories and the semantics of type theory. Theoretical Computer Science, 107:169\u2013207, 1993.","journal-title":"Theoretical Computer Science"},{"key":"31_CR9","unstructured":"Nax P. Mendler. Quotient types via coequalisers in Martin-L\u00f6f's type theory. in the informal proceedings of the workshop on Logical Frameworks, Antibes, May 1990."},{"key":"31_CR10","volume-title":"Programming in Martin-L\u00f6f's Type Theory, An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f's Type Theory, An Introduction. Clarendon Press, Oxford, 1990."},{"key":"31_CR11","unstructured":"Wesley Phoa. An introduction to fibrations, topos theory, the effective topos, and modest sets. Technical Report ECS-LFCS-92-208, LFCS Edinburgh, 1992."},{"key":"31_CR12","unstructured":"Andrew Pitts. Categorical logic. In Handbook of Logic in Computer Science (Vol. VI). Oxford University Press, 199? to appear."},{"key":"31_CR13","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0022-4049(89)90113-8","volume":"57","author":"A. J. Power","year":"1989","unstructured":"A. J. Power. A general coherence result. Journal of Pure and Applied Algebra, 57:165\u2013173, 1989.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"31_CR14","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R. A. G. Seely","year":"1984","unstructured":"Robert A. G. Seely. Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society, 95:33\u201348, 1984.","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Thomas Streicher. Semantics of Type Theory. Birkh\u00e4user, 1991.","DOI":"10.1007\/978-1-4612-0433-6"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022273","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,19]],"date-time":"2021-07-19T23:40:11Z","timestamp":1626738011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022273"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600176","9783540494041"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0022273","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}