Abstract : Nous proposons un système pour typer le traitement des exceptions dans les langages fonctionnels. Ce système est obtenu en exploitant l'isomorphisme de Curry-Howard, à partir de la logique intuitionniste (ou classique) étendue par le connecteur dual de l'implication : la soustraction.
La dualité est utilisée, comme outil de construction et de démonstration, dans l'étude de ce connecteur, sous les quatre angles suivants :
1) la théorie des catégories,
2) les sémantiques algébriques, topologiques et de Kripke,
3) la théorie de la démonstration et
4) l'aspect calculatoire.

Les résultats principaux sont :
1. Les catégories bi-cartésiennes fermées sont nécessairement dégénérées en présence de la soustraction et par conséquent la soustraction n'admet pas d'interprétation dans la catégorie des ensembles.
2. La dualité est une notion intuitionniste dans le sens O% les modèles de
Kripke permettent d'interpréter la soustraction, et de plus coïncident avec les modèles topologiques de la soustraction (dits bi-topologiques).
3. Il existe une traduction très simple de la logique classique vers la logique intuitionniste soustractive. Cette traduction s'étend directement
aux preuves sans coupures du calcul des séquents de Gentzen.
4. La soutraction permet de typer une instruction proche du <> du langage CAML, ceci dans les cadres classiques et intuitionnistes.

Un dernier chapître, indépendant, traite de la réalisabilité modifiée.

Publications internes Litp 1996 / Litp research reports 1996