{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:40:06Z","timestamp":1737063606760,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_39","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T04:15:38Z","timestamp":1180671338000},"page":"554-569","source":"Crossref","is-referenced-by-count":7,"title":["Normalized Types"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Courtieu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"39_CR1","series-title":"Lect Notes Comput Sci","volume-title":"proc TLCArs95","author":"G. Barthe","year":"1995","unstructured":"G. Barthe. Extensions of pure type systems. In proc TLCArs95, volume 902 of lncs. Springer-Verlag, 1995."},{"key":"39_CR2","series-title":"Lect Notes Comput Sci","first-page":"36","volume-title":"Proc. Conf. Computer Science Logic","author":"G. Barthe","year":"1995","unstructured":"G. Barthe and H. Geuvers. Congruence types. In H. Kleine Buening, editor, Proc. Conf. Computer Science Logic, volume 1092 of Lecture Notes in Computer Science, pages 36\u201351, 1995."},{"key":"39_CR3","series-title":"Lect Notes Comput Sci","volume-title":"10th International Conference on Rewriting Techniques and Applications","author":"F. Blanqui","year":"1999","unstructured":"F. Blanqui, J.-P. Jouannaud, and M. Okada. The Calculus of Algebraic Constructions. In Paliath Narendran and Michael Rusinowitch, editors, 10th International Conference on Rewriting Techniques and Applications, volume 1631 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag."},{"key":"39_CR4","doi-asserted-by":"crossref","unstructured":"Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 14\u201325, Warsaw,Poland, June 1997. IEEE Comp. Soc. Press.","DOI":"10.1109\/LICS.1997.614920"},{"key":"39_CR5","volume-title":"R\u00e9flexions sur les quotients","author":"S. Boutin","year":"1997","unstructured":"S. Boutin. R\u00e9flexions sur les quotients. th\u00e9se d\u2019universit\u00e9, Paris 7, April 1997."},{"key":"39_CR6","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and G\u00e9rard Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, February 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"39_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Colog\u201988","author":"T. Coquand","year":"1990","unstructured":"Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In P. Martin-L\u00f6f and G. Mints, editors, Proceedings of Colog\u201988, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990."},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"H. Geuvers. The church rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi. In Proc. 7th IEEE Symp. Logic in Computer Science, Santa Cruz, pages 453\u2013460, 1992.","DOI":"10.1109\/LICS.1992.185556"},{"key":"39_CR9","unstructured":"M. Hofmann. Extensional concepts in intensional type theory. Phd thesis, Edinburgh university, 1995."},{"key":"39_CR10","series-title":"Lect Notes Comput Sci","volume-title":"proc TLCA\u201995","author":"M. Hofmann","year":"1995","unstructured":"M. Hofmann. A simple model for quotient types. In proc TLCA\u201995, volume 902 of lncs. Springer-Verlag, 1995."},{"key":"39_CR11","unstructured":"B. Jacobs. Quotients in simple type theory. Drafts and Notes. http:\/\/www.cwi. nl\/ bjacobs\/ , 1991."},{"key":"39_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Christine Paulin-Mohring. Inductive definitions in the system COQ. In Typed Lambda Calculi and Applications, pages 328\u2013345. Springer-Verlag, 1993. LNCS 664."},{"key":"39_CR13","doi-asserted-by":"crossref","unstructured":"G. Malcolm R. Backhouse, P. Chisholm and E. Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1989.","DOI":"10.1007\/BF01887198"},{"key":"39_CR14","unstructured":"Benjamin Werner. M\u00e9ta-th\u00e9orie du Calcul des Constructions Inductives. Th\u00e8se de doctorat, Univ. Paris VII, 1994."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:02:28Z","timestamp":1737061348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_39","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}