{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:16Z","timestamp":1767927736280,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540509400","type":"print"},{"value":"9783540461180","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-50940-2_39","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:35:41Z","timestamp":1330184141000},"page":"241-256","source":"Crossref","is-referenced-by-count":7,"title":["Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft"],"prefix":"10.1007","author":[{"given":"Robert","family":"Harper","sequence":"first","affiliation":[]},{"given":"Robert","family":"Pollack","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"15_CR1","unstructured":"H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"R. Burstall and Butler Lampson. A kernel language for abstract data types and modules. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 1\u201350. Springer-Verlag, 1984.","DOI":"10.1007\/3-540-13346-1_1"},{"key":"15_CR3","unstructured":"Luca Cardelli. Phase distinctions in type theory. unpublished manuscript."},{"key":"15_CR4","unstructured":"Luca Cardelli. A polymorphic \u03bb-calculus with Type:Type. Technical report, DEC SRC, 1986."},{"key":"15_CR5","series-title":"Technical Report RR","volume-title":"Natural semantics on the computer","author":"D. Cl\u00e9ment","year":"1985","unstructured":"D. Cl\u00e9ment, J. Despeyroux, T. Despeyroux, L. Hascoet, and G. Kahn. Natural semantics on the computer. Technical Report RR 416, INRIA, Sophia-Antipolis, France, June 1985."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"D. Cl\u00e9ment, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple applicative language: Mini-ML. In Proceedings of the Conference on Lisp and Functional Programming, 1986.","DOI":"10.1145\/319838.319847"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and G\u00e9rard Huet. Constructions: a higher-order proof system for mechanizing mathematics. In B. Buchberger, editor, EUROCAL '85: European Conference on Computer Algebra, volume 203 of Lecture Notes in Computer Science, pages 151\u2013184. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"15_CR8","series-title":"Technical Report","volume-title":"An algorithm for checking PL\/CV arithmetical inferences","author":"T. Chan","year":"1977","unstructured":"Tat-Hung Chan. An algorithm for checking PL\/CV arithmetical inferences. Technical Report 77-236, Computer Science Department, University, Ithaca, New York, 1977."},{"key":"15_CR9","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"15_CR10","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert L. Constable, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"15_CR11","unstructured":"Thierry Coquand. Une th\u00e9orie des constructions. PhD thesis, Universit\u00e9 Paris VII, January 1985."},{"key":"15_CR12","unstructured":"Thierry Coquand. An analysis of Girard's paradox. In Proc. of the Symposium on Logic in Computer Science, pages 227\u2013236, Boston, June 1986."},{"key":"15_CR13","unstructured":"Thierry Coquand. Private communication."},{"key":"15_CR14","unstructured":"Robert L. Constable and Daniel R. Zlatin. Report on the type theory (V3) of the programming logic PL\/CV3. In Logics of Programs, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1982."},{"issue":"1","key":"15_CR15","first-page":"72","volume":"7","author":"R. L. Constable","year":"1984","unstructured":"Robert L. Constable and Daniel R. Zlatin. The type theory of PL\/CV3. ACM Transactions on Programming Languages and Systems, 7(1):72\u201393, January 1984.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"T. Despeyroux. Executable specifications of static semantics. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science. Springer-Verlag, June 1984.","DOI":"10.1007\/3-540-13346-1_11"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Luis Damas and Robin Milner. Principal type schemes for functional programs. In Proceedings of the 9th ACM Symposium on the Principles of Programming Languages, pages 207\u2013212, 1982.","DOI":"10.1145\/582153.582176"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Thomas Erhard. A categorical semantics of Constructions. In Proceedings of the Third Annual Symposium on Logic in Computer Science, pages 264\u2013273, Edinburgh, July 1988.","DOI":"10.1109\/LICS.1988.5125"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Paola Giannini and Simona Ronchi della Rocca. Characterization of typings in polymorphic type discipline. In Proceedings of the Third Annual Symposium on Logic in Computer Science, pages 61\u201371, July 1988.","DOI":"10.1109\/LICS.1988.5101"},{"key":"15_CR20","series-title":"Technical Report TR","volume-title":"Impredicative strong existential equivalent to Type:Type","author":"J. G. Hook","year":"1986","unstructured":"James G. Hook and Douglas Howe. Impredicative strong existential equivalent to Type:Type. Technical Report TR 86\u2013760, Cornell University, Ithaca, New York, 1986."},{"key":"15_CR21","unstructured":"Robert Harper, Robin Milner, and Mads Tofte. A type discipline for program modules. In TAPSOFT '87, volume 250 of Lecture Notes in Computer Science. Springer-Verlag, March 1987."},{"key":"15_CR22","unstructured":"Robert Harper, Robin Milner, and Mads Tofte. The definition of Standard ML (version 2). Technical Report ECS-LFCS-88-62, Laboratory for the Foundations of Computer Science, Edinburgh University, August 1988."},{"key":"15_CR23","unstructured":"Douglas Howe. The computational behavior of Girard's paradox. In Proceedings of the Second Symposium on Logic in Computer Science, pages 205\u2013214, Ithaca, New York, June 1987."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"J. Martin E. Hyland and Andrew M. Pitts. The Theory of Constructions: categorical semantics and topos-theoretic models. In Proceedings of the Boulder Conference on Categories in Computer Science, 1988. To appear.","DOI":"10.1090\/conm\/092\/1003199"},{"key":"15_CR25","unstructured":"G\u00e9rard Huet. Extending the Calculus of Constructions with Type:Type. unpublished manuscript, April 1987."},{"key":"15_CR26","unstructured":"Zhaolui Luo. A higher-order calculus and theory abstraction. Technical Report ECS-LFCS-88-57, Laboratory for the Foundations of Computer Science, Edinburgh University, July 1988."},{"key":"15_CR27","unstructured":"Zhaolui Luo. \u221e \u2282 and its metatheory. Technical Report ECS-LFCS-88-58, Laboratory for the Foundations of Computer Science, Edinburgh University, July 1988."},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"David MacQueen. Using dependent types to express modular structure. In Proceedings of the 13th ACM Symposium on the Principles of Programming Languages, 1986.","DOI":"10.1145\/512644.512670"},{"key":"15_CR29","unstructured":"Per Martin-L\u00f6f. A theory of types. Unpublished manuscript."},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium, '73, pages 73\u2013118, Amsterdam, 1973. North-Holland.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175, Amsterdam, 1982. North-Holland.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"15_CR32","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory. Bibliopolis, Naples, 1984."},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"John Mitchell and Robert Harper. The essence of ML. In Proceedings of the Fifteenth ACM Symposium on Principles of Programming Languages, San Diego, California, January 1988.","DOI":"10.1145\/73560.73563"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"John C. Mitchell. Type inference and type containment. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 257\u2013278. Springer-Verlag, 1984.","DOI":"10.1007\/3-540-13346-1_13"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"John C. Mitchell and Gordon Plotkin. Abstract types have existential type. In Proceedings of the 12th ACM Symposium on the Principles of Programming Languages, 1985.","DOI":"10.1145\/318593.318606"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Albert Meyer and Mark Reinhold. \u2018Type\u2019 is not a type: preliminary report. In Proceedings of the 13th ACM Symposium on the Principles of Programming Languages, 1986.","DOI":"10.1145\/512644.512671"},{"key":"15_CR37","unstructured":"Robert Pollack. The theory of lego. Technical report, Laboratory for the Foundations of Computer Science, Edinburgh University, 1988. To appear."},{"key":"15_CR38","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"B. Russell","year":"1908","unstructured":"Bertrand Russell. Mathematical logic as based on a theory of types. American Journal of Mathematics, 30:222\u2013262, 1908.","journal-title":"American Journal of Mathematics"},{"key":"15_CR39","volume-title":"The Language Theory of AUTOMATH","author":"D. T. Daalen van","year":"1980","unstructured":"Diedrik T. van Daalen. The Language Theory of AUTOMATH. PhD thesis, Technical University of Eindhoven, Eindhoven, Netherlands, 1980."},{"key":"15_CR40","volume-title":"Principia Mathematica, Volume 1","author":"Alfred North Whitehead and Bertrand Russell","year":"1925","unstructured":"Alfred North Whitehead and Bertrand Russell. Principia Mathematica, Volume 1. Cambridge University Press, Cambridge, 1925."}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '89"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50940-2_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:19:15Z","timestamp":1605629955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50940-2_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540509400","9783540461180"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-50940-2_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989]]}}}