On the geometry of computations
On the geometry of intuitionistic S4 proofs.
Polarized category theory, modules, and game semantics.
Pre-adjunctions and lambda-algebraic theories
Predicative algebraic set theory.
Preface to the special volume: “Chu spaces: theory and applications".
Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories.
Quelques aspects de la dualité entre logique et topologie
Qu'est-ce que la logique dans une catégorie ?
Relatively boolean and De Morgan toposes and locales
Relevant Categories and Partial Functions
Sémantique catégorique des constructeurs de types d'ordre supérieur
Sémantique catégorique des types : comprendre le système F
Skew -sets coincide with -posets
Sober spaces and continuations.
Spectra of differential rings
Strong functors and interleaving fixpoints in game semantics
We describe a sequent calculus μLJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients:...
Structuration cognitive et logique intrinsèque
À travers l'étude d'un modèle de représentation des connaissances comme catégorie de faisceaux de traits localement définis ; ce texte montre que la théorie des topoï permet de décrire formellement l'émergence d'une logique intrinsèque à partir d'une approche relationnelle, qu'elle soit structurale ou cognitive. On peut alors caractériser mathématiquement le défaut d'intensionnalité des modèles classiques, et montrer qu'une solution est dans la mathématisation de structures entièrement relationnelles....
Subspaces in abstract Stone duality.
Substitution up to isomorphism