@inproceedings{bbc55c5e6e7e406a89748a62be83af4c,

title = "A λ-to-CL translation for strong normalization",

abstract = "We introduce a simple translation from λ-calculus to combinatory logic (CL) such that: A is an SN λ-term iff the translation result of A is an SN term of CL (the reductions are β-reduction in λ-calculus and weak reduction in CL). None of the conventional translations from λ-calculus to CL satisfy the above property. Our translation provides a simpler SN proof of G{\"o}del{\textquoteright}s λ-calculus by the ordinal number assignment method. By using our translation, we construct a homomorphism from a conditionally partial combinatory algebra which arises over SN λ-terms to a partial combinatory algebra which arises over SN CL-terms.",

author = "Yohji Akama",

year = "1997",

month = jan,

day = "1",

doi = "10.1007/3-540-62688-3_25",

language = "English",

isbn = "3540626883",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "1--10",

editor = "{de Groote}, Philippe and Hindley, {J. Roger}",

booktitle = "Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings",

note = "3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997 ; Conference date: 02-04-1997 Through 04-04-1997",

}