Les représentations graphiques des preuves de la logique linéaire, les proof-nets, permettent de s'abstraire de contraintes inhérentes au calcul des séquents comme la syntaxe et les règles structurelles. La correction (ou prouvabilité) de tels réseaux peut se vérifier à l'aide de critères purement graphiques, comme le critère de Danos-Regnier. Sa simplicité en fait le rend très efficace mais peu compréhensible. Pour donner une preuve de complétude d'un tel critère et tenter de l'expliquer, nous utiliserons une logique différente : MILL. Dans ce système intuitionniste, les règles logiques sont des règles de typage d'un lambda-calcul et les réseaux de preuves ses arbres de syntaxe. Le critère de Danos-Regnier nous permettra de construire un lambda-terme typable à partir du réseau de preuve, assurant ainsi sa validité.