Le lambda-bar-mu-mu-tilde calcul, défini par Curien et Herbelin, est une variante du lambda-mu calcul de Parigot qui fait ressortir des symétries comme termes/contextes et appel par nom/valeur. Du fait que c'est un calcul symétrique, et par là non-déterministe, les techniques usuelles de preuves de normalisation nécessitent quelques ajustements. Ici, on prouve la normalisation forte (SN) du lambda-bar-mu-mu-tilde calcul simplement typé, avec substitutions explicites.
Pour cela, on prouve tout d'abord SN du lambda-bar-mu-mu-tilde calcul simplement typé (par une variante de la technique de réductibilité de Barbanera et Berardi), puis on formalise une technique de preuve de SN via PSN (préservation de la normalisation forte), et on prouve PSN par la technique de perpétuité, formalisée par Bonelli.