Les substitutions explicites sont l'une des façons proposées pour étudier
l'implantation de la beta-réduction et pour coder les preuves dans les
assistants. Ce domaine a connu un regain d'intérêt lorsque Melliès a montré
que le calcul lambda-sigma pouvait ne pas terminer même sur des termes
simplement typés.
Nous présenterons un contre-exemple à la terminaison d'un autre calcul (le
lambda se).
Nous présenterons ensuite un calcul qui a de bonnes propriétés de confluence
et dont on sait prouver la terminaison sur les lambda-termes fortement
normalisables.