{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:23:35Z","timestamp":1770276215551,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540605799","type":"print"},{"value":"9783540477709","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60579-7_2","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:42:40Z","timestamp":1330288960000},"page":"14-38","source":"Crossref","is-referenced-by-count":23,"title":["A short and flexible proof of strong normalization for the calculus of constructions"],"prefix":"10.1007","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"2_CR1","unstructured":"Th. Altenkirch, Yet another Strong Normalization proof for the Calculus of Constructions, Laboratory for Foundations of Computer Science, Manuscript, 11 pp."},{"key":"2_CR2","unstructured":"Th. Altenkirch, Constructions, Inductive types and Strong Normalization proof, Ph. D. Thesis, University of Edinburgh, UK."},{"key":"2_CR3","unstructured":"F. Barbanera, M. Fern\u00e1ndez, J.H. Geuvers, Modularity of Strong Normalization in the lambda-algebraic-cube, manuscript."},{"key":"2_CR4","unstructured":"H.P. Barendregt, The lambda calculus: its syntax and semantics, revised edition. Studies in Logic and the Foundations of Mathematics, North Holland."},{"key":"2_CR5","unstructured":"H.P. Barendregt, Typed lambda calculi. In Abramski et al. (eds.), Handbook of Logic in Computer Science, Oxford Univ. Press."},{"key":"2_CR6","unstructured":"S. Berardi, Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Dept. Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino, Italy."},{"key":"2_CR7","unstructured":"Th. Coquand, Une th\u00e9orie des constructions, Th\u00e8se de troisi\u00e8me cycle, Universit\u00e9 Paris VII, France."},{"key":"2_CR8","unstructured":"Th. Coquand, Metamathematical investigations of a calculus of constructions. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 91\u2013122."},{"key":"2_CR9","unstructured":"Th. Coquand and J. Gallier, A proof of Strong Normalization for the Theory of Constructions using a Kripke-like interpretation, In the Informal Proceedings of the Workshop on Logical Frameworks, Antibes, May 1990."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Th. Coquand and G. Huet, The calculus of constructions, Information and Computation, 76, pp 95\u2013120.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"2_CR11","unstructured":"Th. Coquand and Ch. Paulin-Mohring Inductively defined types, In P. Martin-L\u00f6f and G. Mints editors. COLOG-88: International conference on computer logic, LNCS 411."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"J.H. Geuvers and M.J. Nederhof, A modular proof of strong normalisation for the calculus of constructions. Journal of Functional Programming, vol 1 (2), pp 155\u2013189.","DOI":"10.1017\/S0956796800020037"},{"key":"2_CR13","unstructured":"J.H. Geuvers, Logics and Type Systems, Ph. D. thesis, Universiteit Nijmegen, the Netherlands."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"H. Geuvers and B. Werner, On the Church-Rosser property for Expressive Type Systems and its Consequences for their Metatheoretic Study, in Proceedings of the Ninth Annual Symposium on Logic in Computer Science, Paris, France, IEEE Computer Society, pp 320\u2013329.","DOI":"10.1109\/LICS.1994.316057"},{"key":"2_CR15","unstructured":"On Girard's \u201cCandidats de Reductibilit\u00e9\u201d. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 123\u2013204."},{"key":"2_CR16","unstructured":"J.-Y. Girard, Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII, France."},{"key":"2_CR17","unstructured":"J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Camb. Tracts in Theoretical Computer Science 7, Cambridge University Press."},{"key":"2_CR18","volume-title":"PhD. thesis","author":"H. Goguen","year":"1994","unstructured":"H. Goguen, A Typed Operational Semantics for Type Theory, PhD. thesis, University of Edinburgh, UK, 1994."},{"key":"2_CR19","unstructured":"Z. Luo, An Extended Calculus of Constructions, Ph. D. Thesis, University of Edinburgh, UK."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Z. Luo, ECC: An extended Calculus of Constructions. Proc. of the fourth ann. symp. on Logic in Comp. Science, Asilomar, Cal. IEEE, pp 386\u2013395.","DOI":"10.1109\/LICS.1989.39193"},{"key":"2_CR21","unstructured":"P. Martin-L\u00f6f, Intuitionistic Type Theory, Studies in Proof theory, Bibliopolis, Napoli."},{"key":"2_CR22","unstructured":"B. Nordstr\u00f6m, K. Petersson, J.M. Smith, Programming in Martin-L\u00f6f's Type Theory. Oxford University Press."},{"key":"2_CR23","unstructured":"L. Ong and E. Ritter, A generic Strong Normalization argument: application to the Calculus of Constructions, University of Cambridge Computer Laboratory, Manuscript, 19 pp."},{"key":"2_CR24","unstructured":"A guide to polymorphic types. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 387\u2013420."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"W.W. Tait, Infinitely long terms of transfinite type. In Formal Systems and Recursive Functions, eds. J.N. Crossley and M.A.E. Dummett, North-Holland.","DOI":"10.1016\/S0049-237X(08)71689-6"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"W.W. Tait, A realizability interpretation of the theory of species. In Proceedings of Logic Colloquium, ed. R. Parikh, LNM 453, pp 240\u2013251.","DOI":"10.1007\/BFb0064875"},{"key":"2_CR27","unstructured":"J. Terlouw, Strong Normalization in type systems: a model theoretic approach, In the Dirk van Dalen Festschrift, Eds. H. Barendregt, M. Bezem and J.W. Klop, Department of Philosophy, Utrecht University, the Netherlands, pp 161\u2013190."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60579-7_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:05:40Z","timestamp":1742598340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60579-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605799","9783540477709"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-60579-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}