Ma thèse [For03] a principalement portée sur l’étude du filtrage dans les langages de programmation fonctionnelle (OCaml, Haskell,…) et les assistants à la preuve (COQ,…).

J’ai proposé, durant cette thèse, deux formalisme :

• Le premier de ces formalismes [For02a, For02b], le λ P_w-calcul, est une extension du λ-calcul possédant des opérateurs explicites de filtrage (à la ML) et de substitution (à la λ_σ). Le λ P_w-calcul est prouvé fortement normalisant sur les expressions bien typées et confluent.
• Le second des ces formalismes [FK03, FK07], proposé en collaboration avec Délia Kesner, permet l’utilisation de filtre à la ML dans le cadre de la réécriture d’ordre supérieur. Un critère de confluence pour les systèmes de réécriture d’ordre supérieur avec motifs est défini et prouvé correct.

• Publications

This document was translated from L^AT_EX by H^EV^EA.