Nous savons maintenant qu'il existe dans la nature des modèles de la logique classique qui sont aux catégories ce que les algèbres de Boole sont aux ensembles ordonnés. Durant des années on a cru que de tels êtres ne pouvaient exister, étant donné le célèbre 171 paradoxe de Joyal 187 : une catégorie cartésienne fermée ne peut être équipée d'une négation symétrique. Les premiers exemples étaient des catégories de réseaux de démonstrations. Nous avons ensuite construit des sémantiques dénotationnelles pour la logique classique qui ressemblent beaucoup aux espaces cohérents. L'exposé se concentrera sur les propriétés essentielles que tous ces modèles possèdent, en d'autres termes sur les raisons pour quoi ça marche. Ces modèles nous mènent à nous poser des questions sur l'universalité de l'isomorphisme de Curry-Howard : il existe des façons de dénoter des preuves en logique classique pour lesquelles le processus de normalisation ne correspond pas au calcul en programmation fonctionnelle. Les connaissances en théorie des catégories que nous supposons de la part de l'autitoire sont absolument minimales : les définitions de catégorie, foncteur et transformation naturelle.