{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:08:06Z","timestamp":1774987686915,"version":"3.50.1"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2016,8,10]],"date-time":"2016-08-10T00:00:00Z","timestamp":1470787200000},"content-version":"unspecified","delay-in-days":9263,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1991,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a modular proof of strong normalization for the Calculus of Constructions of Coquand and Huet (1985, 1988). This result was first proved by Coquand (1986), but our proof is more perspicious. The method consists of a little juggling with some systems in the cube of Barendregt (1989), which provides a fine structure of the calculus of constructions. It is proved that the strong normalization of the calculus of constructions is equivalent with the strong normalization of <jats:italic>F<\/jats:italic>\u03c9.<\/jats:p><jats:p>In order to give the proof, we first establish some properties of various type systems. Therefore, we present a general framework of typed lambda calculi, including many well-known ones.<\/jats:p>","DOI":"10.1017\/s0956796800020037","type":"journal-article","created":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T18:01:05Z","timestamp":1558116065000},"page":"155-189","source":"Crossref","is-referenced-by-count":71,"title":["Modular proof of strong normalization for the calculus of constructions"],"prefix":"10.1017","volume":"1","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[]},{"given":"Mark-Jan","family":"Nederhof","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,8,10]]},"reference":[{"key":"S0956796800020037_ref014","volume-title":"Proceedings of the second Scandinavian Logic Symposium","author":"Girard","year":"1971"},{"key":"S0956796800020037_ref008","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0956796800020037_ref004","unstructured":"Barendregt H. P. and Dekkers W. 1990. Typed Lambda Calculi."},{"key":"S0956796800020037_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15983-5_13"},{"key":"S0956796800020037_ref006","volume-title":"Towards a mathematical analysis of type dependence in Coquand-Huet calculus of constructions and the other systems in Barendregt's cube","author":"Berardi","year":"1988"},{"key":"S0956796800020037_ref001","volume-title":"The Lambda calculus, its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"S0956796800020037_ref013","unstructured":"Girard J.-Y. 1972. Interpretation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e8se de Doctorat d'Etat, Universit\u00e9 de Paris VIII, France."},{"key":"S0956796800020037_ref019","first-page":"240","volume-title":"Logic Colloquium. Volume 453 of Lecture Notes in Mathematics","author":"Tait","year":"1975"},{"key":"S0956796800020037_ref018","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"S0956796800020037_ref005","unstructured":"Barendsen E. 1989. Representation of logic, data types and recursive functions in typed lambda calculi. Masters Thesis, Faculty of Mathematics and Computer Science, University of Nijmegen, The Netherlands."},{"key":"S0956796800020037_ref011","first-page":"95","volume-title":"Information and Computation","author":"Coquand","year":"1988"},{"key":"S0956796800020037_ref016","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S0956796800020037_ref015","volume-title":"Proc. Symposium on Logic in Computer Science, Ithaca, New York","author":"Harper","year":"1987"},{"key":"S0956796800020037_ref002","volume-title":"Proc. 3rd Italian Conference on Theoretical Computer Science","author":"Barendregt","year":"1989"},{"key":"S0956796800020037_ref007","first-page":"579","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"de Bruijn","year":"1980"},{"key":"S0956796800020037_ref017","volume-title":"and its strong normalization","author":"Luo","year":"1988"},{"key":"S0956796800020037_ref012","unstructured":"Geuvers H. 1988. The interpretation of logics in type systems. Masters Thesis, Faculty of Mathematics and Computer Science, Catholic University Nijmegen, The Netherlands."},{"key":"S0956796800020037_ref020","volume-title":"Een nadere bewijstheoretische analyse van GSTT's","author":"Terlouw","year":"1989"},{"key":"S0956796800020037_ref003","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1990"},{"key":"S0956796800020037_ref009","volume-title":"Metamathematical Investigations of a Calculus of Constructions","author":"Coquand","year":"1986"},{"key":"S0956796800020037_ref021","volume-title":"Sterke normalisatie in C \u00e0 la Tait","author":"Terlouw","year":"1989"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800020037","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T18:01:30Z","timestamp":1558116090000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800020037\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,4]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1991,4]]}},"alternative-id":["S0956796800020037"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800020037","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,4]]}}}