Curien, Pierre-Louis; Ríos, Alejandro Un résultat de complétude pour les substitutions explicites. (A completeness result for explicit substitutions). (French) Zbl 0717.68053 C. R. Acad. Sci., Paris, Sér. I 312, No. 6, 471-476 (1991). Summary: We establish a completeness result of \(\lambda\sigma\)-calculus with respect to \(\lambda\)-calculus. Specifically we construct an interpretation of \(\lambda\sigma\)-calculus into \(\lambda\)-calculus, which is such that a source term is typable iff its translation is typable (with the same type). We restrict ourselves to first-order types. Cited in 1 Document MSC: 68W30 Symbolic computation and algebraic computation 03B40 Combinatory logic and lambda calculus Keywords:substitution; closure operation PDFBibTeX XMLCite \textit{P.-L. Curien} and \textit{A. Ríos}, C. R. Acad. Sci., Paris, Sér. I 312, No. 6, 471--476 (1991; Zbl 0717.68053)