Types Simples, Logique et Coercions Implicites

Nous definissons un systeme general de coercions implicites dans les types simples et donnons un algorithme d'inference de type. Ceci est realise grâce a une logique adequate, inspiree de la logique lineaire, pour laquelle nous prouvons l'elimination des coupures.