{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:54:13Z","timestamp":1773096853236,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440390","type":"print"},{"value":"9783540456858","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_9","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"115-130","source":"Crossref","is-referenced-by-count":8,"title":["Explicit Universes for the Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"Judica\u00ebl","family":"Courant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"9_CR1","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. Inf. Comp., 76:95\u2013120, 1988.","journal-title":"Inf. Comp."},{"key":"9_CR2","unstructured":"Thierry Coquand. An analysis of Girard\u2019s paradox. In Proceedings of the First Symposium on Logic in Computer Science, Cambridge, MA, June 1986. IEEE Comp. Soc. Press."},{"key":"9_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/3-540-62688-3_32","volume-title":"Typed Lambda Calculi and Applications\u2019 97","author":"J. Courant","year":"1997","unstructured":"Judica\u00ebl Courant. A Module Calculus for Pure Type Systems. In Typed Lambda Calculi and Applications\u2019 97, Lecture Notes in Computer Science, pages 112\u2013128. Springer-Verlag, 1997."},{"key":"9_CR4","unstructured":"Judica\u00ebl Courant. MC2: A Module Calculus for Pure Type Systems. Research Report 1292, LRI, September 2001."},{"key":"9_CR5","unstructured":"James G. Hook and Douglas J. Howe. Impredicative Strong Existential Equivalent to Type:Type. Technical Report TR86-760, Cornell University, 1986."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"R. Harper and R. Pollack. Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions. Theoretical Computer Science, 89(1), 1991.","DOI":"10.1016\/0304-3975(90)90108-T"},{"key":"9_CR7","volume-title":"The Nuprl Proof Development System, Version 4.I Reference Manual and User\u2019s Guide","author":"P. B. Jackson","year":"1994","unstructured":"Paul B. Jackson. The Nuprl Proof Development System, Version 4.I Reference Manual and User\u2019s Guide. Cornell University, Ithaca, NY, 1994."},{"key":"9_CR8","unstructured":"Paul B. Jackson. Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, 1995."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Zhaohui Luo. ECC: an Extended Calculus of Constructions. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, California, 1989. IEEE Comp. Soc. Press.","DOI":"10.1109\/LICS.1989.39193"},{"key":"9_CR10","unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"9_CR12","unstructured":"M. Takahashi. Parallel reductions in \u03bb-calculus. Technical report, Department of Information Science, Tokyo Institute of Technology, 1993. Internal report."},{"key":"9_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Types for Proofs and Programs: International Workshop TYPES\u201993","author":"L.S. Benthem Jutting van","year":"1993","unstructured":"L.S. van Benthem Jutting, J. McKinna, and R. Pollack. Checking algorithms for pure type systems. In Types for Proofs and Programs: International Workshop TYPES\u201993, volume 806 of Lecture Notes in Computer Science, May 1993."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:42:33Z","timestamp":1683844953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}