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.