## Un résultat de complétude pour les substitutions explicites. (A completeness result for explicit substitutions).(French)Zbl 0717.68053

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.

### MSC:

 68W30 Symbolic computation and algebraic computation 03B40 Combinatory logic and lambda calculus

### Keywords:

substitution; closure operation