Nous présenterons une extension du système F+η (introduit par John C. Mitchell) avec un mécanisme d'exceptions typées. Le comportement calculatoire de notre mécanisme s'éloigne des comportements habituels puisque la réduction des exceptions y suit une discipline en appel par nom. Nous montrerons que cette particularité nous amène à considérer une nouvelle notion, la "corruption", pour le typage de ces exceptions. L'introduction de cette notion amenant entre autre chose une certaine modularité du système de type.
Une fois notre extension présentée, nous en exhiberons un modèle de réalisabilité (défini par orthogonalité) qui nous permettra d'établir des résultats de correction du typage et de normalisation (faible). Nous montrerons en particulier que l'interprétation de la flèche dans ce modèle n'est pas standard (et ne peut l'être).