Dans cet expos� nous pr�senterons deux formalismes de r��criture permettant l'utilisation de filtrage ��� la ML��.
Le premier de ces formalismes, le lambda P calcul, est une extension du calcul lambda sigma d'une part et du calcul TPC d'autre part. A ces titres, ce calcul traite de mani�re compl�tement explicite les notions de substitution et de filtrage. Nous montrerons qu'il poss�de les propri�t�s de normalisation forte sur les termes typ�s et de confluence.
Le second est un formalisme de r��criture d'ordre sup�rieur fond� sur les (S)ERS. Ce formalisme autorise la d�finition de syst�mes de r��criture utilisant la notion de filtrage. Nous donnerons un crit�re syntaxique de confluence pour de tels syst�mes.