Un calcul de substitutions explicites est une extension du lambda-calcul dans lequel la substitution est intégrée au calcul au même titre que le sont l`abstraction ou l`application, alors que dans le lambda-calcul, la substitution fait partie de la métathéorie, c`est-à-dire qu`elle est déf...