{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:26:13Z","timestamp":1767929173457,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540282310","type":"print"},{"value":"9783540318972","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11538363_12","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T13:35:33Z","timestamp":1127828133000},"page":"151-166","source":"Crossref","is-referenced-by-count":9,"title":["On the Role of Type Decorations in the Calculus of Inductive Constructions"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Barras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"12_CR1","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0304-3975(00)00175-4","volume":"266","author":"D. Aspinall","year":"2001","unstructured":"Aspinall, D., Compagnoni, A.: Subtyping dependent types. Theor. Comput. Sci.\u00a0266(1-2), 273\u2013309 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR2","volume-title":"Handbook of Logic in Computer Science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, Gabbay, Maibaum (eds.) Handbook of Logic in Computer Science, vol.\u00a02, Clarendon, Oxford (1992)"},{"key":"12_CR3","unstructured":"Barras, B.: Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. PhD thesis, Universit\u00e9 Paris 7 (1999)"},{"issue":"2","key":"12_CR4","first-page":"191","volume":"14","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Coquand, T.: On the equational theory of non-normalizing pure type systems. Journal of Functional Programming\u00a014(2), 191\u2013209 (2004)","journal-title":"Journal of Functional Programming"},{"issue":"5","key":"12_CR5","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1017\/S0956796800003750","volume":"10","author":"G. Barthe","year":"2000","unstructured":"Barthe, G., S\u00f8rensen, M.: Domain-free pure type systems. Journal of Functional Programming\u00a010(5), 412\u2013452 (2000)","journal-title":"Journal of Functional Programming"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: TACS, pp. 515\u2013529 (1997)","DOI":"10.1007\/BFb0014565"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Castagna, G., Chen, G.: Dependent types with subtyping and late-bound overloading. INFCTRL: Information and Computation (formerly Information and Control), 168 (2001)","DOI":"10.1006\/inco.2001.3128"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0029962","volume-title":"Mathematical Foundations of Computer Science 1997","author":"G. Chen","year":"1997","unstructured":"Chen, G.: Subtyping calculus of construction. In: Privara, I., Ru\u017ei\u010dka, P. (eds.) MFCS 1997. LNCS, vol.\u00a01295, Springer, Heidelberg (1997)"},{"key":"12_CR9","first-page":"235","volume-title":"International Conference on Functional Programming 2002","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming 2002, pp. 235\u2013246. ACM Press, New York (2002)"},{"key":"12_CR10","unstructured":"Leroy, X., Doligez, J.V.D.: The Objective Caml System. Institut National de Recherche en Informatique et en Automatique, Software and documentation (August 2004), Available on the Web http:\/\/caml.inria.fr\/"},{"key":"12_CR11","unstructured":"Luo, Z.: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1990)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. Journal of Automated Reasoning\u00a023(3-4) (November 1999)","DOI":"10.1023\/A:1006294005493"},{"key":"12_CR13","unstructured":"Paulin-Mohring, C.: Extraction de programmes dans le Calcul des Constructions. Ph.d. thesis, Paris 7 (January 1989)"},{"key":"12_CR14","unstructured":"Pollack, R.: The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, Univ. of Edinburgh (1994)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Streicher, T.: Semantics of Type Theory: Correctness, Completeness, and Independence Results. Birkhauser (1991)","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"12_CR16","unstructured":"The Coq development team. The coq proof assistant reference manual v7.2. Technical Report 255, INRIA, France, march (2002), http:\/\/coq.inria.fr\/doc8\/main.html"},{"key":"12_CR17","unstructured":"Werner, B.: Une Th\u00e9orie de Constructions Inductives. Ph.d. thesis, Universit\u00e9 Paris 7 (May 1994)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11538363_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:13:36Z","timestamp":1605644016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11538363_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540282310","9783540318972"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11538363_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}