RésuméUn paradigme en vogue en informatique théorique exploite l'analogie entre les formules et les types et traite une deduction A_l … A_n → B comme une opération plurisortale. On propose ici d'étendre cette analogie aux déductions de la forme A_l … A_n →, où la place à droite de la flèche est vide. D'un point de vue logique, une telle déduction constitue une réfutation de la conjonction desformules qui se trouvent à gauche de la flèche. On défend l'idée qu'ilfaut, selon ce paradigme étendu, interpréter la flèche comme assignant à n'importe quelle séquence a_l … a_n, où a_i est de type A_i, le type des valeurs de vérite correspondantes. Pour que cela fonctionne, cependant, il faut abandonner la règle structurale de l'affaiblissement à droite de la flèche (cette règle est entièrement abandonnée en logique de la pertinence). La négation de A est alors interprétée comme l'ensemble puissance de A et la complétude fonctionnelle habituelle s'identifie au schème de compréhension avec extensionnalitè.