Abstract FR:

Le lambda-sigma-calcul (ls) a deux sortes de termes: terme propre et substitution. Le ls-calcul est confluent sur les termes clos, mais il n'est pas localement confluent sur tous les termes. La confluence locale est atteinte en ajoutant quatre regles. Le calcul ainsi obtenu est appele lsp, et sa non-confluence sur la totalite des termes a ete recemment montree. Cependant, le lsp-calcul et le lsp-calcul extensionnel sont confluents sur l'ensemble des termes semi-clos (ceux qui n'admettent que de variables de sorte terme propre). Ces resultats sont obtenus en utilisant la methode d'interpretation; pour l'appliquer, la normalisation forte du sp-calcul de substitutions associe est necessaire. Une nouvelle technique est developpee pour l'assurer. Dans le cadre type, on introduit une interpretation du ls-calcul type du premier ordre dans le lambda-calcul, pour laquelle la correction et la completude sont etablies. La normalisation forte du tau-calcul est un probleme ouvert. Un premier pas est franchi en montrant la normalisation faible. Le lambda-nu-calcul (ln) traite la substitution explicite en abandonnant la notation de de bruijn. La correction de ln ne peut etre obtenue qu'en imposant des restrictions aux variables du terme de depart. On introduit une condition et une strategie de reduction qui la preserve, pour laquelle ln est correct et confluent modulo alpha-conversion