Les espaces cohérents de Jean-Yves Girard et les espaces de finitude de Thomas Ehrhard sont obtenus à partir d'une base « similaire » : l'orthogonalité.
Je commencerais par rappeler comment ça marche (parce que c'est intéressant et pas très compliqué), puis je passerais à une structure mixte qui permet de générer des espaces de finitude « simples » à partir d'espaces cohérents.
Cette construction contient tous les exemples usuels d'espaces de finitude et de plus, elle commute avec les opérations logiques (⅋, ⊗, ⊕, &, ⊸, !, …) Un des aspects intéressants est l'utilisation du théorème de Ramsey infini pour démontrer certaines propriétés de cette construction.
Je finirais par expliquer comment on tombe sur une notion qui généralise les fonctions stable de Berry pour permettre d'interpréter une version simple du λ-calcul algébrique de Lionel, Thomas et consorts.
Remarques : j'essaierais, autant que possible, de ne pas supposer connue toute la logique linéaire. Les deux premiers tiers de mon exposé devraient donc être « self-contained »...