{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:05:10Z","timestamp":1773097510843,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540590484","type":"print"},{"value":"9783540491781","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014055","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"216-234","source":"Crossref","is-referenced-by-count":16,"title":["A simple model for quotient types"],"prefix":"10.1007","author":[{"given":"Martin","family":"Hofmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"15_CR1","unstructured":"Thorsten Altenkirch. Constructions, normalization, and inductive types. PhD thesis, University of Edinburgh, 1994."},{"key":"15_CR2","unstructured":"Hendrik Barendregt. Functional programming and lambda calculus. Handbook of Theoretical Computer Science, Volume B."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Michael Beeson. Foundations of Constructive Mathematics. Springer, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Errett Bishop and Douglas Bridges. Constructive Analysis. Springer, 1985.","DOI":"10.1007\/978-3-642-61667-9"},{"key":"15_CR5","unstructured":"J. Cartmell. Generalized algebraic theories and contextual categories. PhD thesis, Univ. Oxford, 1978."},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Thierry Coquand and G\u00e9rard Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"15_CR7","unstructured":"Robert Constable et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986."},{"key":"15_CR8","unstructured":"Herman Geuvers and Benjamin Werner. On the Church-Rosser property for expressive type systems. LICS '94."},{"key":"15_CR9","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge, 1993."},{"key":"15_CR10","unstructured":"Martin Hofmann. Elimination of extensionality for Martin-L\u00f6f type theory. LNCS 806."},{"key":"15_CR11","unstructured":"Bart Jacobs. Quotients in Simple Type Theory. submitted."},{"key":"15_CR12","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":"15_CR13","doi-asserted-by":"crossref","unstructured":"J. Lambek and P. Scott. Introduction to Higher-Order Categorical Logic. Cambridge, 1985.","DOI":"10.1090\/conm\/030\/749773"},{"key":"15_CR14","unstructured":"I. Moerdijk and S. Mac Lane. Sheaves in Geometry and Logic. Springer, 1992."},{"key":"15_CR15","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":"15_CR16","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":"15_CR17","unstructured":"Andrew Pitts. Categorical logic. In Handbook of Theoretical Computer Science. Elsevier Science, 199? to appear."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Jan Smith. The independence of Peano's fourth axiom from Martin-L\u00f6fs type theory without universes. Journal of Symbolic Logic, 53(3), 1988.","DOI":"10.2307\/2274575"},{"key":"15_CR19","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","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014055","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:38:01Z","timestamp":1586579881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014055"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0014055","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}