![]() New notions of reduction and non-semantic proofs of β-strong normalization in typed λ-calculi. 185 of Lecture Notes in Computer Science, Springer-Verlag, 1985, pp. In Mathematical Foundations of Computer Software, H. “Delayability” in proofs of strong normalizability in the typed lambda calculus. ![]() Report, Department of Computer Science, University of Copenhagen, March 1999. Functional interpretations and normalization. Proof Theory and Logical Complexity, Bibliopolis, 1987, Vol. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. 664 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. In Typed Lambda Calculus and Applications, M. ![]() The Lambda Calculus: Its Syntax and Semantics, 2nd revised edition. In Handbook of Logic in Computer Science, S. For instance, we prove the main property of Gandy's translation without reference to functionals using instead ideas from Klop's translation.īarendregt, H.P. For instance, in the case of Xi's translation, this other translation is a thunkification translation.įinally we compare the above techniques in some detail to the intimately related techniques by de Vrijer and Girard.Ī main contribution of the paper is to compare the techniques of Gandy, Klop, and Girard in detail. Having established this, which is easy, the fact that all the translations can be used to reduce strong normalization to weak normalization can be obtained from a single, general result concerning permutative inner interpretations.įurthermore, we show that each of the translations can be obtained as the composition of Klop's well-known ι-translation and some other translation of independent interest. We show that all the translations, in some cases via adjustments, are special cases of a generic scheme of translations, known as permutative inner interpretations. We present variants of such techniques due to Klop, Sørensen, Xi, Gandy, and Loader. This paper offers a systematic account of techniques to infer strong normalization from weak normalization that make use of syntactic translations from λ-terms to λ I-terms.
0 Comments
Leave a Reply. |
Details
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |