{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:20Z","timestamp":1725665000432},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_25","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:48:27Z","timestamp":1330296507000},"page":"1-10","source":"Crossref","is-referenced-by-count":4,"title":["A \u03bb-to-CL translation for strong normalization"],"prefix":"10.1007","author":[{"given":"Yohji","family":"Akama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Y. Akama. On Mints' reduction for ccc-calculus. In Bezem and Groote [7], pages 1\u201312.","DOI":"10.1007\/BFb0037094"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"T. Altenkirch. Proving strong normalization of CC by modifying realizability semantics. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, volume 806 of Lecture Notes on Computer Science, pages 3\u201318. Springer, 1994.","DOI":"10.1007\/3-540-58085-9_70"},{"key":"1_CR3","unstructured":"H. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, second edition, 1984."},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"M. Beeson. Foundations of Constructive Mathematics. Springer, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"I. Bethke and J. W. Klop. Collapsing partial combinatory algebras. In G. Dowek, J.Heering, K.Meinke, and B.M\u00f6ller, editors, Higher-Order Algebra, Logic, and Term Rewriting, volume 1074 of Lecture Notes on Computer Science, pages 57\u201373. Springer, 1996.","DOI":"10.1007\/3-540-61254-8_19"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"I. Bethke, J. W. Klop, and R. de Vrijer. Completing partial combinatory algebras with unique head-normal forms. In Logic in Computer Science, pages 448\u2013454. IEEE Computer Society press, 1996.","DOI":"10.1109\/LICS.1996.561461"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"M. Bezem and J.F. Groote, editors. Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science. Springer, 1993.","DOI":"10.1007\/BFb0037093"},{"key":"1_CR8","unstructured":"H. B. Curry, J. R. Hindley, and J. P. Seldin. Combinatory Logic, Volume II. Studies in Logic and the Foundations of Mathematics. North-Holland, 1972."},{"key":"1_CR9","unstructured":"J.R. Hindley and J.P. Seldin. Introduction to Combinators and Lambda-calculus. Cambridge University Press, 1986."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"W.A. Howard. Assignment of ordinals to terms for primitive recursive functionals of finite type. In A. Kino, J. Myhill, and R. Vesley, editors, Intuitionism and Proof Theory, pages 443\u2013458. North-Holland, 1970.","DOI":"10.1016\/S0049-237X(08)70770-5"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland and C.-H. L. Ong. Modified realizability toposes and strong normalization proofs (extended abstract). In Bezem and Groote [7], pages 179\u2013194.","DOI":"10.1007\/BFb0037106"},{"key":"1_CR12","unstructured":"J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 2\u2013117. Oxford University Press, 1992."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"K. Sch\u00fctte. Proof Theory. Springer, 1977. (translated by J. Crossley from the German.).","DOI":"10.1007\/978-3-642-66473-1"},{"issue":"1","key":"1_CR14","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1002\/spe.4380090105","volume":"9","author":"D. A. Turner","year":"1979","unstructured":"D. A. Turner. A new implementation technique for applicative languages. Software Practice and Experience, 9(1):31\u201349, January 1979.","journal-title":"Software Practice and Experience"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:13:58Z","timestamp":1605647638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}