{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:09Z","timestamp":1725474489019},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097796","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T09:27:48Z","timestamp":1164360468000},"page":"254-276","source":"Crossref","is-referenced-by-count":6,"title":["A generic normalisation proof for pure type systems"],"prefix":"10.1007","author":[{"given":"Paul-Andr\u00e9","family":"Melli\u00e8s","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Werner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"14_CR1","unstructured":"T. Altenkirch. Constructions, Inductive Types and Strong Normalization. Ph.D. Thesis, University of Edinburgh, 1993."},{"key":"14_CR2","unstructured":"H. Barendregt. Lambda Calculi with Types. In Handbook of Logic in Computer Science, Vol II, Elsevier, 1992"},{"key":"14_CR3","unstructured":"G. Barthe, P.-A. Melli\u00e8s. On the Subject Reduction property for algebraic type systems. In Proceedings CSL'96, LNCS 1258, Springer Verlag, 1996."},{"key":"14_CR4","unstructured":"G. Dowek, G. Huet and B. Werner. On the Definition of the \u03b7-long Normal Form in Type Systems of the Cube. Submitted to publication. See also http:\/\/pauillac.inria.fr\/~werner\/,1996."},{"issue":"2","key":"14_CR5","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers et M.-J. Nederhof. A modular proof of strong normalization for the Calculus of Constructions. Journal of Functional Programming, 1 (2):155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"key":"14_CR6","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e8se d'Etat, Universit\u00e9 Paris 7, 1972."},{"key":"14_CR7","unstructured":"J. W. Klop, Combinatory Reduction Systems. Ph.D. Thesis, Utrecht University, 1980."},{"key":"14_CR8","unstructured":"G. Longo and E. Moggi. Constructive Natural Deduction and its \u03c9-set Interpretation."},{"key":"14_CR9","unstructured":"Z. Luo. An Extended Calculus of Constructions. Ph.D. Thesis, University of Edinburgh, 1990."},{"key":"14_CR10","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Studies in Proof Theory, Bibliopolis, 1984."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"W. W. Tait. A realizability interpretation of the theory of species. In Logic Colloquium, R. Parikh Ed. LNM 453, Springer-Verlag, 1975.","DOI":"10.1007\/BFb0064875"},{"key":"14_CR12","unstructured":"J. Terlouw. Strong Normalization in Type Systems: a model theoretical approach. In Dirk van Dalen Festschrift, Henk Barendregt, Marc Bezem and Jan Willem Klop Eds. Dept. of Philosophy, Utrecht University, 1993."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097796","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T23:20:29Z","timestamp":1587252029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097796"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0097796","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}