{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T23:40:23Z","timestamp":1736293223692,"version":"3.32.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":39,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540582770"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0049336","type":"book-chapter","created":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T18:58:16Z","timestamp":1141671496000},"page":"261-279","source":"Crossref","is-referenced-by-count":1,"title":["A generic strong normalization argument: Application to the Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"C. -H. L.","family":"Ong","sequence":"first","affiliation":[]},{"given":"E.","family":"Ritter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"J. B\u00e9nabou. Fibred categories and the foundations of na\u00efve category theory. J. Symb. Logic, pages 10\u201337, 1985.","key":"17_CR1","DOI":"10.2307\/2273784"},{"key":"17_CR2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"H. Barendregt. Introduction to generalized type systems. J. Functional Prog., 1:125\u2013154, 1991.","journal-title":"J. Functional Prog."},{"unstructured":"K. Petersson B. Nordstr\u00f6m and J. M. Smith. Programming in Martin-L\u00f6f Type Theory: An Introduction. Oxford University Press, 1990.","key":"17_CR3"},{"doi-asserted-by":"crossref","unstructured":"J. Cartmell. Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32, 1986.","key":"17_CR4","DOI":"10.1016\/0168-0072(86)90053-9"},{"doi-asserted-by":"crossref","unstructured":"A. Carboni, P. J. Freyd, and A. Scedrov. A categorical approach to realizability and polymorphic types. In M. Main et al., editor, Mathematical Foundations of Programming Language Semantics. Springer, 1988. LNCS Vol. 298.","key":"17_CR5","DOI":"10.1007\/3-540-19020-1_2"},{"key":"17_CR6","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Info. and Comp., 76:95\u2013120, 1988.","journal-title":"Info. and Comp."},{"doi-asserted-by":"crossref","unstructured":"Th. Ehrhard. A categorical semantics of constructions. In Ieee Annual Symp. Logic in Computer Science. Computer Society Press, 1988.","key":"17_CR7","DOI":"10.1109\/LICS.1988.5125"},{"doi-asserted-by":"crossref","unstructured":"Y. Ershov. Theorie der numerierungen I & II. Z. Math. Logik., 19 & 21, 1973 & 1975.","key":"17_CR8","DOI":"10.1002\/malq.19750210164"},{"unstructured":"J. Gallier. Realizability, covers, and sheaves. unpublished manuscript, available by anonymous ftp, 1993.","key":"17_CR9"},{"doi-asserted-by":"crossref","unstructured":"H. Geuvers. The church-rosser property for \u03b2\u03b7-reduction in typed lambda calculi. In Proc. 7th Annual Ieee Symp. Logic in Computer Science, pages 453\u2013460. Computer Societyy Press, 1992.","key":"17_CR10","DOI":"10.1109\/LICS.1992.185556"},{"unstructured":"H. Geuvers. Logics and Type Systems. PhD thesis, University of Nijmegen, 1993.","key":"17_CR11"},{"unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et elimination des coupures dans l'arithmetique d'order sup\u00e9rieur. Th\u00e8se de Doctorat d'Etat, Paris, 1972.","key":"17_CR12"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.-Y. Girard","year":"1986","unstructured":"J.-Y. Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45:159\u2013192, 1986.","journal-title":"Theoretical Computer Science"},{"unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989. Cambridge Tracts in Theoretical Computer Science 7.","key":"17_CR14"},{"key":"17_CR15","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1017\/S0305004100057534","volume":"88","author":"J. M. E. Hyland","year":"1980","unstructured":"J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88:205\u2013232, 1980.","journal-title":"Math. Proc. Camb. Phil. Soc."},{"key":"17_CR16","series-title":"LNCS Vol. 664","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/BFb0037106","volume-title":"Proc. Conf. Type Lambda Calculus and Applications","author":"J. M. E. Hyland","year":"1993","unstructured":"J. M. E. Hyland and C.-H. L. Ong. Modified realizability topos and strong normalization proofs. In Proc. Conf. Type Lambda Calculus and Applications, Utrecht, March 93, pages 179\u2013194. Springer-Verlag, 1993. LNCS Vol. 664."},{"key":"17_CR17","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1090\/conm\/092\/1003199","volume":"92","author":"J. M. E. Hyland","year":"1989","unstructured":"J. M. E. Hyland and A. M. Pitts. The theory of constructions: Categorical semantics and topos-theoretic models. Contemporary Mathematics, 92:137\u2013199, 1989.","journal-title":"Contemporary Mathematics"},{"key":"17_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1112\/plms\/s3-60.1.1","volume":"60","author":"J. M. E. Hyland","year":"1990","unstructured":"J. M. E. Hyland, E. P. Robinson, and G. Rosolini. The discrete objects in the effective topos. Proc. London Math. Soc. (3), 60:1\u201336, 1990.","journal-title":"Proc. London Math. Soc. (3)"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0168-0072(88)90018-8","volume":"40","author":"J. M. E. Hyland","year":"1988","unstructured":"J. M. E. Hyland. A small complete category. Annals of Pure and Applied Logic, 40:135\u2013165, 1988.","journal-title":"Annals of Pure and Applied Logic"},{"key":"17_CR20","volume-title":"PhD thesis","author":"B. Jacobs","year":"1991","unstructured":"B. Jacobs. Categorical Type Theory. PhD thesis, Catholic University of Nijmegen, 1991."},{"unstructured":"G. Kreisel. Interpretation of analysis by means of constructive functionals of finite type. In A Heyting, editor, Constructivity in Mathematics. North-Holland, 1959.","key":"17_CR21"},{"doi-asserted-by":"crossref","unstructured":"G. Longo and E. Moggi. Constructive natural deducation and its \u201c\u03c9-set\u201d interpretation. Math. Structures in Comp. Sc., ?, 1992.","key":"17_CR22","DOI":"10.1017\/S0960129500001298"},{"key":"17_CR23","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0890-5401(91)90062-7","volume":"90","author":"Z. Luo","year":"1991","unstructured":"Z. Luo. A higher-order calculus and theory abstraction. Information and Computation, 90:107\u2013137, 1991.","journal-title":"Information and Computation"},{"key":"17_CR24","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A theory of type polymorphism in programming. J. Computer and System Science, 17:348\u2013375, 1978.","journal-title":"J. Computer and System Science"},{"unstructured":"P. Martin-L\u00f6f. About models for intuitionistic type theories and the notion of definitional equality, paper read at the Orl\u00e9ans Logic Conference, 1972.","key":"17_CR25"},{"unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984. Studies in Proof Theory Series.","key":"17_CR26"},{"unstructured":"W. Phoa. An introduction to fibration, topos theory and the effective topos and modest sets. Technical Report ECS-LFCS-92-208, Edinburgh University, 1992.","key":"17_CR27"},{"key":"17_CR28","volume-title":"LNCS. Vol. 287","author":"A. M. Pitts","year":"1987","unstructured":"A. M. Pitts. Polymorphism is set-theoretical, constructively. In D. H. Pitt et al., editor, Proc. Conf. Category Theory and Computer Science, Edinburgh, Berlin, 1987. Springer-Verlag. LNCS. Vol. 287."},{"unstructured":"A. M. Pitts. Categorical semantics of dependent types. Talk given at Sri Menlo Park, 2 June, 1989.","key":"17_CR29"},{"doi-asserted-by":"crossref","unstructured":"R. A. G. Seely. Locally cartesian closed categories and type theory. Math. Proc. Camb. Phil. Soc., 95, 1984.","key":"17_CR30","DOI":"10.1017\/S0305004100061284"},{"key":"17_CR31","doi-asserted-by":"crossref","first-page":"969","DOI":"10.2307\/2273831","volume":"52","author":"R. A. G. Seely","year":"1987","unstructured":"R. A. G. Seely. Categorical semantics for higher order polymorphic lambda calculus. J. Symb. Logic, 52:969\u2013989, 1987.","journal-title":"J. Symb. Logic"},{"doi-asserted-by":"crossref","unstructured":"T. Streicher. Semantics of Type Theory: Correctness, Completeness and Independence Results. Birkh\u00e4user, 1991.","key":"17_CR32","DOI":"10.1007\/978-1-4612-0433-6"},{"unstructured":"T. Streicher. Truly intensional models of type theory arising from modified realizability, dated 25 May '92 mailing list at CATEGORIES@mta.ca, 1992.","key":"17_CR33"},{"key":"17_CR34","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"W. W. Tait. Intensional interpretation of functionals of finite type i. J. Symb. Logic, 32:198\u2013212, 1967.","journal-title":"J. Symb. Logic"},{"unstructured":"P. Taylor. Recursive Domains, Indexed Catgory Theory and Polymorphism. PhD thesis, Dpmms, University of Cambridge, 1987.","key":"17_CR35"},{"unstructured":"J. Terlouw. Strong normalization in type systems: a model-theoretic approach. In Dirk van Dalen Festschrift, pages 161\u2013190. Dept. of Philosophy, Utrecht Univ., 1993.","key":"17_CR36"},{"unstructured":"S. Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991.","key":"17_CR37"},{"doi-asserted-by":"crossref","unstructured":"A. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer, 1973. Springer Lecture Notes in Mathematics 344.","key":"17_CR38","DOI":"10.1007\/BFb0066739"},{"unstructured":"R. Turner. Constructive Foundations for Functional Languages. McGraw Hill, 1991.","key":"17_CR39"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0049336.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T23:00:39Z","timestamp":1736290839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0049336"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540582770"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/bfb0049336","relation":{},"subject":[]}}